linearscan 0.10.2 → 0.11
raw patch · 17 files changed
+949/−1164 lines, 17 files
Files
- LinearScan.hs +8/−10
- LinearScan/Allocate.hs +28/−3
- LinearScan/Assign.hs +327/−355
- LinearScan/Blocks.hs +9/−12
- LinearScan/Build.hs +55/−64
- LinearScan/Lib.hs +0/−32
- LinearScan/List1.hs +4/−0
- LinearScan/LiveSets.hs +34/−38
- LinearScan/Loops.hs +261/−316
- LinearScan/Main.hs +59/−57
- LinearScan/Monad.hs +0/−13
- LinearScan/Resolve.hs +134/−238
- LinearScan/State.hs +4/−0
- LinearScan/State0.hs +0/−4
- LinearScan/UsePos.hs +3/−3
- LinearScan/Verify.hs +22/−18
- linearscan.cabal +1/−1
LinearScan.hs view
@@ -394,8 +394,8 @@ -- | From the point of view of this library, a basic block is nothing more -- than an ordered sequence of operations. data BlockInfo m blk1 blk2 op1 op2 = BlockInfo- { blockId :: blk1 -> m Int- , blockSuccessors :: blk1 -> m [Int]+ { blockId :: blk1 -> Int+ , blockSuccessors :: blk1 -> [Int] , splitCriticalEdge :: blk1 -> blk1 -> m (blk1, blk1) , blockOps :: blk1 -> ([op1], [op1], [op1]) , setBlockOps :: blk1 -> [op2] -> [op2] -> [op2] -> blk2@@ -417,7 +417,7 @@ where go _ [] = return "" go pos (b:bs) = do- bid <- LinearScan.blockId binfo b+ let bid = LinearScan.blockId binfo b let (liveIn, liveOut) = case M.lookup bid ls of Nothing -> (S.empty, S.empty) Just s -> (S.fromList (LS.blockLiveIn s),@@ -433,9 +433,7 @@ => LinearScan.BlockInfo m blk1 blk2 op1 op2 -> LS.BlockInfo (m Any) blk1 blk2 op1 op2 fromBlockInfo (BlockInfo a b c d e) =- LS.Build_BlockInfo- (\r1 -> U.unsafeCoerce (a r1))- (\r1 -> U.unsafeCoerce (b r1))+ LS.Build_BlockInfo a b (\r1 r2 -> U.unsafeCoerce (c r1 r2)) (\blk -> let (x, y, z) = d blk in ((x, y), z)) e @@ -483,10 +481,10 @@ "spill (r" ++ show fr ++ " v" ++ show tv ++ ")" ++ showSplit b show (LS.RSRestore fv tr b) = "restore (r" ++ show tr ++ " v" ++ show fv ++ ")" ++ showSplit b- show (LS.RSAllocReg fv tr b) =- "<reserve> (r" ++ show tr ++ " v" ++ show fv ++ ")" ++ showSplit b- show (LS.RSFreeReg fr tv b) =- "<release> (r" ++ show fr ++ " v" ++ show tv ++ ")" ++ showSplit b+ 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) =
LinearScan/Allocate.hs view
@@ -16,7 +16,6 @@ import qualified LinearScan.Context as Context import qualified LinearScan.Cursor as Cursor import qualified LinearScan.Interval as Interval-import qualified LinearScan.Lib as Lib import qualified LinearScan.Maybe as Maybe import qualified LinearScan.Morph as Morph import qualified LinearScan.ScanState as ScanState@@ -309,13 +308,39 @@ Prelude.Left err -> Prelude.Left err; Prelude.Right s -> Prelude.Right s} +dep_foldl_invE :: (a2 -> Eqtype.Equality__Coq_type) -> a2 -> ([]+ Eqtype.Equality__Coq_sort) -> Prelude.Int -> (a2 -> []+ Eqtype.Equality__Coq_sort) -> (a2 -> a2 -> () ->+ Eqtype.Equality__Coq_sort -> Eqtype.Equality__Coq_sort) ->+ (a2 -> () -> Eqtype.Equality__Coq_sort -> ([]+ Eqtype.Equality__Coq_sort) -> () -> Prelude.Either + a1 (Specif.Coq_sig2 a2)) -> Prelude.Either a1 a2+dep_foldl_invE e b v n q f f0 =+ let {filtered_var = (,) v n} in+ case filtered_var of {+ (,) l n0 ->+ case l of {+ [] -> Prelude.Right b;+ (:) y ys ->+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ -> Prelude.Right+ b)+ (\n' ->+ let {filtered_var0 = f0 b __ y ys __} in+ case filtered_var0 of {+ Prelude.Left err -> Prelude.Left err;+ Prelude.Right s ->+ let {ys' = Prelude.map (f b s __) ys} in+ dep_foldl_invE e s ys' n' q f f0})+ n0}}+ checkActiveIntervals :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int -> Morph.SState () () () checkActiveIntervals maxReg pre pos = Morph.withScanStatePO maxReg pre (\sd _ -> Context.ibind (\e -> let {- eres = Lib.dep_foldl_invE (\s ->+ eres = dep_foldl_invE (\s -> Eqtype.prod_eqType (Fintype.ordinal_eqType (ScanState.nextInterval maxReg s)) (Fintype.ordinal_eqType maxReg)) sd@@ -405,7 +430,7 @@ Morph.withScanStatePO maxReg pre (\sd _ -> Context.ibind (\e -> let {- eres = Lib.dep_foldl_invE (\s ->+ eres = dep_foldl_invE (\s -> Eqtype.prod_eqType (Fintype.ordinal_eqType (ScanState.nextInterval maxReg s)) (Fintype.ordinal_eqType maxReg)) sd
LinearScan/Assign.hs view
@@ -118,9 +118,9 @@ k (Blocks.saveOp maxReg mDict oinfo sreg svid); Resolve.Restore dvid dreg b -> k (Blocks.restoreOp maxReg mDict oinfo dvid dreg);- Resolve.AllocReg v p b ->+ Resolve.AllocReg v p -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing;- Resolve.FreeReg p v b ->+ Resolve.FreeReg p v -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.AssignReg v p -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing;@@ -240,377 +240,349 @@ 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 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\suxs ->- case IntMap.coq_IntMap_lookup bid liveSets of {- Prelude.Just bls ->- let {liveIns = LiveSets.blockLiveIn bls} in- let {liveOuts = LiveSets.blockLiveOut bls} in- case let {- fwds = Maybe.maybe [] IntSet.coq_IntSet_toList- (IntMap.coq_IntMap_lookup bid- (Loops.forwardBranches loops))}- in- let {- bwds = Maybe.maybe [] IntSet.coq_IntSet_toList- (IntMap.coq_IntMap_lookup bid- (Loops.backwardBranches loops))}- in- (,)- (List1.concat- (Prelude.map (\b ->- case IntMap.coq_IntMap_lookup b liveSets of {- Prelude.Just x1 -> (:)- (LiveSets.blockLastOpId x1) [];- Prelude.Nothing -> []})- ((Prelude.++) fwds bwds)))- (List1.concat- (Prelude.map (\b ->- case IntMap.coq_IntMap_lookup b liveSets of {- Prelude.Just x1 -> (:)- (LiveSets.blockFirstOpId x1) [];- Prelude.Nothing -> []}) suxs)) of {- (,) froms tos ->- case Maybe.fromMaybe ((,) [] [])- (IntMap.coq_IntMap_lookup bid mappings) of {- (,) begMoves endMoves ->- let {- k = setAllocations maxReg mDict oinfo useVerifier- allocs}- in- let {- resolutions = \pos toFroms moves ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->- 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 pos- useVerifier moves))- (case toFroms of {- Prelude.Left froms0 ->- Monad.forM_ (State0.coq_StateT_Monad mDict)- froms0 (\b ->- Verify.verifyTransitions maxReg mDict pos- allocs useVerifier moves b ((Prelude.succ)- pos));- Prelude.Right tos0 ->- Monad.forM_ (State0.coq_StateT_Monad mDict)- tos0 (\e ->- Verify.verifyTransitions maxReg mDict pos- allocs useVerifier moves pos e)})}- in- Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ let {bid = Blocks.blockId mDict binfo blk} in+ let {suxs = Blocks.blockSuccessors mDict binfo blk} in+ case IntMap.coq_IntMap_lookup bid liveSets of {+ Prelude.Just bls ->+ let {liveIns = LiveSets.blockLiveIn bls} in+ let {liveOuts = LiveSets.blockLiveOut bls} in+ case let {+ fwds = Maybe.maybe [] IntSet.coq_IntSet_toList+ (IntMap.coq_IntMap_lookup bid+ (Loops.forwardBranches loops))}+ in+ let {+ bwds = Maybe.maybe [] IntSet.coq_IntSet_toList+ (IntMap.coq_IntMap_lookup bid+ (Loops.backwardBranches loops))}+ in+ (,)+ (List1.concat+ (Prelude.map (\b ->+ case IntMap.coq_IntMap_lookup b liveSets of {+ Prelude.Just x1 -> (:) (LiveSets.blockLastOpId x1)+ [];+ Prelude.Nothing -> []}) ((Prelude.++) fwds bwds)))+ (List1.concat+ (Prelude.map (\b ->+ case IntMap.coq_IntMap_lookup b liveSets of {+ Prelude.Just x1 -> (:) (LiveSets.blockFirstOpId x1)+ [];+ Prelude.Nothing -> []}) suxs)) of {+ (,) froms tos ->+ case Maybe.fromMaybe ((,) [] [])+ (IntMap.coq_IntMap_lookup bid mappings) of {+ (,) begMoves endMoves ->+ let {+ k = setAllocations maxReg mDict oinfo useVerifier allocs}+ in+ let {+ resolutions = \pos toFroms moves ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ 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 pos+ useVerifier moves))+ (case toFroms of {+ Prelude.Left froms0 ->+ Monad.forM_ (State0.coq_StateT_Monad mDict) froms0+ (\b ->+ Verify.verifyTransitions maxReg mDict pos allocs+ useVerifier moves b ((Prelude.succ) pos));+ Prelude.Right tos0 ->+ Monad.forM_ (State0.coq_StateT_Monad mDict) tos0+ (\e ->+ Verify.verifyTransitions maxReg mDict pos allocs+ useVerifier moves pos e)})}+ in+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\opsb' ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\opid0 -> Monad.bind (State0.coq_StateT_Monad mDict)- (\opsb' ->+ (\bmoves -> Monad.bind (State0.coq_StateT_Monad mDict)- (\opid0 ->+ (\opsm' -> Monad.bind (State0.coq_StateT_Monad mDict)- (\bmoves ->- Monad.bind (State0.coq_StateT_Monad mDict)- (\opsm' ->+ (\z ->+ case z of {+ (,) opse' opid1 -> Monad.bind (State0.coq_StateT_Monad mDict)- (\z ->- case z of {- (,) opse' opid1 ->- Monad.bind- (State0.coq_StateT_Monad mDict)- (\x2 ->- case opsb' of {- [] ->- let {- opsm'' = (Prelude.++) bmoves opsm'}- 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 opsm'}- 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- useVerifier bid liveOuts)})- (case opse of {- [] ->+ (\x2 ->+ case opsb' of {+ [] ->+ let {+ opsm'' = (Prelude.++) bmoves opsm'}+ 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 opsm'}+ 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+ useVerifier bid liveOuts)})+ (case opse of {+ [] ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\opid1 ->+ Applicative.pure+ (State0.coq_StateT_Applicative mDict)+ ((,) [] opid1))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y)+ (_assnOpId y))) mDict);+ (:) e es ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\xs ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\opid1 -> Monad.bind (State0.coq_StateT_Monad mDict)- (\opid1 ->+ (\x2 -> Applicative.pure (State0.coq_StateT_Applicative- mDict) ((,) [] opid1))- (Lens.use- (Lens.stepdownl' (\_ y ->- (Prelude..) (_verExt maxReg y)- (_assnOpId y))) mDict);- (:) e es ->- Monad.bind- (State0.coq_StateT_Monad mDict)- (\xs ->- Monad.bind- (State0.coq_StateT_Monad mDict)- (\opid1 ->- Monad.bind- (State0.coq_StateT_Monad mDict)- (\x2 ->- Applicative.pure- (State0.coq_StateT_Applicative- mDict) ((,)- ((Prelude.++) xs x2) opid1))- (k- (resolutions opid1- (Prelude.Right tos)- endMoves) (Seq.last e es)))- (Lens.use- (Lens.stepdownl' (\_ y ->- (Prelude..) (_verExt maxReg y)- (_assnOpId y))) mDict))- (Monad.concatMapM+ mDict) ((,) ((Prelude.++) xs x2)+ opid1))+ (k+ (resolutions opid1 (Prelude.Right+ tos) endMoves) (Seq.last e es)))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y)+ (_assnOpId y))) mDict))+ (Monad.concatMapM+ (State0.coq_StateT_Applicative mDict)+ (k+ (Applicative.pure (State0.coq_StateT_Applicative- mDict)- (k- (Applicative.pure- (State0.coq_StateT_Applicative- mDict) []))- (Seq.belast e es))}))- (Monad.concatMapM- (State0.coq_StateT_Applicative mDict)- (k- (Applicative.pure- (State0.coq_StateT_Applicative mDict)- [])) opsm))- (resolutions (Prelude.pred opid0)- (Prelude.Left froms) begMoves))- (Lens.use- (Lens.stepdownl' (\_ y ->- (Prelude..) (_verExt maxReg y)- (_assnOpId y))) mDict))- (Monad.concatMapM- (State0.coq_StateT_Applicative mDict)- (k- (Applicative.pure- (State0.coq_StateT_Applicative mDict) []))- opsb))- (Verify.verifyBlockBegin maxReg mDict opid- useVerifier bid liveIns loops)}};- Prelude.Nothing ->- case let {- fwds = Maybe.maybe [] IntSet.coq_IntSet_toList- (IntMap.coq_IntMap_lookup bid- (Loops.forwardBranches loops))}- in- let {- bwds = Maybe.maybe [] IntSet.coq_IntSet_toList- (IntMap.coq_IntMap_lookup bid- (Loops.backwardBranches loops))}- in- (,)- (List1.concat- (Prelude.map (\b ->- case IntMap.coq_IntMap_lookup b liveSets of {- Prelude.Just x1 -> (:)- (LiveSets.blockLastOpId x1) [];- Prelude.Nothing -> []})- ((Prelude.++) fwds bwds)))- (List1.concat- (Prelude.map (\b ->- case IntMap.coq_IntMap_lookup b liveSets of {- Prelude.Just x1 -> (:)- (LiveSets.blockFirstOpId x1) [];- Prelude.Nothing -> []}) suxs)) of {- (,) froms tos ->- case Maybe.fromMaybe ((,) [] [])- (IntMap.coq_IntMap_lookup bid mappings) of {- (,) begMoves endMoves ->- let {- k = setAllocations maxReg mDict oinfo useVerifier- allocs}- in- let {- resolutions = \pos toFroms moves ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->- 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 pos- useVerifier moves))- (case toFroms of {- Prelude.Left froms0 ->- Monad.forM_ (State0.coq_StateT_Monad mDict)- froms0 (\b ->- Verify.verifyTransitions maxReg mDict pos- allocs useVerifier moves b ((Prelude.succ)- pos));- Prelude.Right tos0 ->- Monad.forM_ (State0.coq_StateT_Monad mDict)- tos0 (\e ->- Verify.verifyTransitions maxReg mDict pos- allocs useVerifier moves pos e)})}- in- Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ mDict) [])) (Seq.belast e es))}))+ (Monad.concatMapM+ (State0.coq_StateT_Applicative mDict)+ (k+ (Applicative.pure+ (State0.coq_StateT_Applicative mDict) []))+ opsm))+ (resolutions (Prelude.pred opid0) (Prelude.Left+ froms) begMoves))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y) (_assnOpId y)))+ mDict))+ (Monad.concatMapM+ (State0.coq_StateT_Applicative mDict)+ (k+ (Applicative.pure+ (State0.coq_StateT_Applicative mDict) []))+ opsb))+ (Verify.verifyBlockBegin maxReg mDict opid useVerifier+ bid liveIns loops)}};+ Prelude.Nothing ->+ case let {+ fwds = Maybe.maybe [] IntSet.coq_IntSet_toList+ (IntMap.coq_IntMap_lookup bid+ (Loops.forwardBranches loops))}+ in+ let {+ bwds = Maybe.maybe [] IntSet.coq_IntSet_toList+ (IntMap.coq_IntMap_lookup bid+ (Loops.backwardBranches loops))}+ in+ (,)+ (List1.concat+ (Prelude.map (\b ->+ case IntMap.coq_IntMap_lookup b liveSets of {+ Prelude.Just x1 -> (:) (LiveSets.blockLastOpId x1)+ [];+ Prelude.Nothing -> []}) ((Prelude.++) fwds bwds)))+ (List1.concat+ (Prelude.map (\b ->+ case IntMap.coq_IntMap_lookup b liveSets of {+ Prelude.Just x1 -> (:) (LiveSets.blockFirstOpId x1)+ [];+ Prelude.Nothing -> []}) suxs)) of {+ (,) froms tos ->+ case Maybe.fromMaybe ((,) [] [])+ (IntMap.coq_IntMap_lookup bid mappings) of {+ (,) begMoves endMoves ->+ let {+ k = setAllocations maxReg mDict oinfo useVerifier allocs}+ in+ let {+ resolutions = \pos toFroms moves ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ 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 pos+ useVerifier moves))+ (case toFroms of {+ Prelude.Left froms0 ->+ Monad.forM_ (State0.coq_StateT_Monad mDict) froms0+ (\b ->+ Verify.verifyTransitions maxReg mDict pos allocs+ useVerifier moves b ((Prelude.succ) pos));+ Prelude.Right tos0 ->+ Monad.forM_ (State0.coq_StateT_Monad mDict) tos0+ (\e ->+ Verify.verifyTransitions maxReg mDict pos allocs+ useVerifier moves pos e)})}+ in+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\opsb' ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\opid0 -> Monad.bind (State0.coq_StateT_Monad mDict)- (\opsb' ->+ (\bmoves -> Monad.bind (State0.coq_StateT_Monad mDict)- (\opid0 ->+ (\opsm' -> Monad.bind (State0.coq_StateT_Monad mDict)- (\bmoves ->- Monad.bind (State0.coq_StateT_Monad mDict)- (\opsm' ->+ (\z ->+ case z of {+ (,) opse' opid1 -> Monad.bind (State0.coq_StateT_Monad mDict)- (\z ->- case z of {- (,) opse' opid1 ->- Monad.bind- (State0.coq_StateT_Monad mDict)- (\x2 ->- case opsb' of {- [] ->- let {- opsm'' = (Prelude.++) bmoves opsm'}- 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 opsm'}- 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- useVerifier bid IntSet.emptyIntSet)})- (case opse of {- [] ->+ (\x2 ->+ case opsb' of {+ [] ->+ let {+ opsm'' = (Prelude.++) bmoves opsm'}+ 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 opsm'}+ 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+ useVerifier bid IntSet.emptyIntSet)})+ (case opse of {+ [] ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\opid1 ->+ Applicative.pure+ (State0.coq_StateT_Applicative mDict)+ ((,) [] opid1))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y)+ (_assnOpId y))) mDict);+ (:) e es ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\xs ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\opid1 -> Monad.bind (State0.coq_StateT_Monad mDict)- (\opid1 ->+ (\x2 -> Applicative.pure (State0.coq_StateT_Applicative- mDict) ((,) [] opid1))- (Lens.use- (Lens.stepdownl' (\_ y ->- (Prelude..) (_verExt maxReg y)- (_assnOpId y))) mDict);- (:) e es ->- Monad.bind- (State0.coq_StateT_Monad mDict)- (\xs ->- Monad.bind- (State0.coq_StateT_Monad mDict)- (\opid1 ->- Monad.bind- (State0.coq_StateT_Monad mDict)- (\x2 ->- Applicative.pure- (State0.coq_StateT_Applicative- mDict) ((,)- ((Prelude.++) xs x2) opid1))- (k- (resolutions opid1- (Prelude.Right tos)- endMoves) (Seq.last e es)))- (Lens.use- (Lens.stepdownl' (\_ y ->- (Prelude..) (_verExt maxReg y)- (_assnOpId y))) mDict))- (Monad.concatMapM+ mDict) ((,) ((Prelude.++) xs x2)+ opid1))+ (k+ (resolutions opid1 (Prelude.Right+ tos) endMoves) (Seq.last e es)))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y)+ (_assnOpId y))) mDict))+ (Monad.concatMapM+ (State0.coq_StateT_Applicative mDict)+ (k+ (Applicative.pure (State0.coq_StateT_Applicative- mDict)- (k- (Applicative.pure- (State0.coq_StateT_Applicative- mDict) []))- (Seq.belast e es))}))- (Monad.concatMapM- (State0.coq_StateT_Applicative mDict)- (k- (Applicative.pure- (State0.coq_StateT_Applicative mDict)- [])) opsm))- (resolutions (Prelude.pred opid0)- (Prelude.Left froms) begMoves))- (Lens.use- (Lens.stepdownl' (\_ y ->- (Prelude..) (_verExt maxReg y)- (_assnOpId y))) mDict))- (Monad.concatMapM- (State0.coq_StateT_Applicative mDict)- (k- (Applicative.pure- (State0.coq_StateT_Applicative mDict) []))- 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.blockSuccessors mDict binfo blk)))- (Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict- (State0.coq_StateT_Monad mDict)- (Blocks.blockId mDict binfo blk)))+ mDict) [])) (Seq.belast e es))}))+ (Monad.concatMapM+ (State0.coq_StateT_Applicative mDict)+ (k+ (Applicative.pure+ (State0.coq_StateT_Applicative mDict) []))+ opsm))+ (resolutions (Prelude.pred opid0) (Prelude.Left+ froms) begMoves))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y) (_assnOpId y)))+ mDict))+ (Monad.concatMapM+ (State0.coq_StateT_Applicative mDict)+ (k+ (Applicative.pure+ (State0.coq_StateT_Applicative mDict) []))+ opsb))+ (Verify.verifyBlockBegin maxReg mDict opid useVerifier+ bid IntSet.emptyIntSet loops)}}}) (Lens.modifyStateT (\_ y -> (Prelude..) (_verExt maxReg y) (_assnBlockEnd y)) ((Prelude.+) opid
LinearScan/Blocks.hs view
@@ -105,24 +105,21 @@ type BlockId = Prelude.Int data BlockInfo m blockType1 blockType2 opType1 opType2 =- Build_BlockInfo (blockType1 -> m) (blockType1 -> m) (blockType1 ->- blockType1 -> m) - (blockType1 -> (,) ((,) ([] opType1) ([] opType1)) ([] opType1)) (blockType1- -> ([]- opType2) ->- ([]- opType2) ->- ([]- opType2) ->- blockType2)+ Build_BlockInfo (blockType1 -> BlockId) (blockType1 -> [] BlockId) + (blockType1 -> blockType1 -> m) (blockType1 -> (,)+ ((,) ([] opType1) ([] opType1))+ ([] opType1)) (blockType1 -> ([] opType2) ->+ ([] opType2) -> ([] opType2)+ -> blockType2) -blockId :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 -> a1+blockId :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 -> BlockId blockId h b = case b of { Build_BlockInfo blockId0 blockSuccessors0 splitCriticalEdge0 blockOps0 setBlockOps0 -> blockId0} -blockSuccessors :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 -> a1+blockSuccessors :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 -> []+ BlockId blockSuccessors h b = case b of { Build_BlockInfo blockId0 blockSuccessors0 splitCriticalEdge0 blockOps0
LinearScan/Build.hs view
@@ -13,10 +13,8 @@ import qualified Data.Functor.Identity import qualified Hask.Utils -import qualified LinearScan.Applicative as Applicative import qualified LinearScan.Blocks as Blocks import qualified LinearScan.Datatypes as Datatypes-import qualified LinearScan.Functor as Functor import qualified LinearScan.IntMap as IntMap import qualified LinearScan.IntSet as IntSet import qualified LinearScan.Interval as Interval@@ -496,41 +494,36 @@ reduceBlocks :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> Loops.LoopState -> (IntMap.IntMap IntSet.IntSet) ->- (IntMap.IntMap LiveSets.BlockLiveSets) -> Prelude.Int -> a5+ (IntMap.IntMap LiveSets.BlockLiveSets) -> Prelude.Int ->+ BuildState reduceBlocks maxReg mDict binfo oinfo blocks loops varUses liveSets pos =- let {- _evar_0_ = \pos0 ->- Applicative.pure (Monad.is_applicative mDict) (newBuildState pos0)}- in+ let {_evar_0_ = \pos0 -> newBuildState pos0} in let { _evar_0_0 = \b blocks0 iHbs pos0 -> let {sz = Blocks.blockSize mDict binfo b} in let { _evar_0_0 = \_ -> (Prelude.flip (Prelude.$)) __ (\_ ->- Monad.bind mDict (\bid ->- let {- outs = case IntMap.coq_IntMap_lookup bid liveSets of {- Prelude.Just ls -> LiveSets.blockLiveOut ls;- Prelude.Nothing -> IntSet.emptyIntSet}}- in- let {- ranges = emptyPendingRanges maxReg pos0 ((Prelude.+) pos0 sz) outs}- in- let {- pending = reduceBlock maxReg mDict binfo oinfo pos0 bid b loops- varUses ranges}- in- Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict))- (mergeIntoSortedRanges pos0 ((Prelude.+) pos0 sz) pending)- (iHbs ((Prelude.+) pos0 sz))) (Blocks.blockId mDict binfo b))}+ (Prelude.flip (Prelude.$)) (Blocks.blockId mDict binfo b) (\bid ->+ (Prelude.flip (Prelude.$))+ (case IntMap.coq_IntMap_lookup bid liveSets of {+ Prelude.Just ls -> LiveSets.blockLiveOut ls;+ Prelude.Nothing -> IntSet.emptyIntSet}) (\outs ->+ (Prelude.flip (Prelude.$))+ (emptyPendingRanges maxReg pos0 ((Prelude.+) pos0 sz) outs)+ (\ranges ->+ (Prelude.flip (Prelude.$))+ (reduceBlock maxReg mDict binfo oinfo pos0 bid b loops+ varUses ranges) (\pending ->+ mergeIntoSortedRanges pos0 ((Prelude.+) pos0 sz) pending+ (iHbs ((Prelude.+) pos0 sz)))))))} in let {_evar_0_1 = \_ -> iHbs pos0} in case (Prelude.<=) ((Prelude.succ) 0) sz of { Prelude.True -> _evar_0_0 __; Prelude.False -> _evar_0_1 __}} in- Datatypes.list_rect _evar_0_ _evar_0_0 blocks pos+ Datatypes.list_rec _evar_0_ _evar_0_0 blocks pos compileIntervals :: Prelude.Int -> Prelude.Int -> BuildState -> (,) ScanState.FixedIntervalsType@@ -579,7 +572,7 @@ buildIntervals :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> Loops.LoopState -> (IntMap.IntMap- LiveSets.BlockLiveSets) -> a5+ LiveSets.BlockLiveSets) -> ScanState.ScanStateSig buildIntervals maxReg mDict binfo oinfo blocks loops liveSets = let { add_unhandled_interval = \ss i ->@@ -599,44 +592,42 @@ in case blocks of { [] ->- Applicative.pure (Monad.is_applicative mDict)- (ScanState.packScanState maxReg ScanState.InUse- (ScanState.Build_ScanStateDesc 0 (unsafeCoerce Vector0.vnil)- (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []));+ ScanState.packScanState maxReg ScanState.InUse+ (ScanState.Build_ScanStateDesc 0 (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []); (:) b bs ->- Monad.bind mDict (\varUses ->- Monad.bind mDict (\reduced ->- case compileIntervals maxReg 0 reduced of {- (,) regs vars ->- let {- s2 = ScanState.packScanState maxReg ScanState.Pending- (ScanState.Build_ScanStateDesc- (ScanState.nextInterval maxReg- (ScanState.Build_ScanStateDesc 0- (unsafeCoerce Vector0.vnil)- (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))- (ScanState.intervals maxReg (ScanState.Build_ScanStateDesc- 0 (unsafeCoerce Vector0.vnil)- (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))- regs- (ScanState.unhandled maxReg (ScanState.Build_ScanStateDesc- 0 (unsafeCoerce Vector0.vnil)- (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))- (ScanState.active maxReg (ScanState.Build_ScanStateDesc 0- (unsafeCoerce Vector0.vnil)- (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))- (ScanState.inactive maxReg (ScanState.Build_ScanStateDesc 0- (unsafeCoerce Vector0.vnil)- (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))- (ScanState.handled maxReg (ScanState.Build_ScanStateDesc 0- (unsafeCoerce Vector0.vnil)- (Vector0.vconst maxReg Prelude.Nothing) [] [] [] [])))}- in- let {s3 = IntMap.coq_IntMap_foldl add_unhandled_interval s2 vars}- in- Applicative.pure (Monad.is_applicative mDict)- (ScanState.packScanState maxReg ScanState.InUse ( s3))})- (reduceBlocks maxReg mDict binfo oinfo ((:) b bs) loops varUses- liveSets 0))- (Loops.computeVarReferences maxReg mDict binfo oinfo ((:) b bs) loops)}+ let {+ varUses = Loops.computeVarReferences maxReg mDict binfo oinfo ((:) b bs)+ loops}+ in+ let {+ reduced = reduceBlocks maxReg mDict binfo oinfo ((:) b bs) loops varUses+ liveSets 0}+ in+ case compileIntervals maxReg 0 reduced of {+ (,) regs vars ->+ let {+ s2 = ScanState.packScanState maxReg ScanState.Pending+ (ScanState.Build_ScanStateDesc+ (ScanState.nextInterval maxReg (ScanState.Build_ScanStateDesc 0+ (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))+ (ScanState.intervals maxReg (ScanState.Build_ScanStateDesc 0+ (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] [])) regs+ (ScanState.unhandled maxReg (ScanState.Build_ScanStateDesc 0+ (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))+ (ScanState.active maxReg (ScanState.Build_ScanStateDesc 0+ (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))+ (ScanState.inactive maxReg (ScanState.Build_ScanStateDesc 0+ (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))+ (ScanState.handled maxReg (ScanState.Build_ScanStateDesc 0+ (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] [])))}+ in+ let {s3 = IntMap.coq_IntMap_foldl add_unhandled_interval s2 vars} in+ ScanState.packScanState maxReg ScanState.InUse ( s3)}}
LinearScan/Lib.hs view
@@ -12,36 +12,4 @@ import qualified Data.Functor.Identity import qualified Hask.Utils -import qualified LinearScan.Specif as Specif-import qualified LinearScan.Eqtype as Eqtype---__ :: any-__ = Prelude.error "Logical or arity value used"--dep_foldl_invE :: (a2 -> Eqtype.Equality__Coq_type) -> a2 -> ([]- Eqtype.Equality__Coq_sort) -> Prelude.Int -> (a2 -> []- Eqtype.Equality__Coq_sort) -> (a2 -> a2 -> () ->- Eqtype.Equality__Coq_sort -> Eqtype.Equality__Coq_sort) ->- (a2 -> () -> Eqtype.Equality__Coq_sort -> ([]- Eqtype.Equality__Coq_sort) -> () -> Prelude.Either - a1 (Specif.Coq_sig2 a2)) -> Prelude.Either a1 a2-dep_foldl_invE e b v n q f f0 =- let {filtered_var = (,) v n} in- case filtered_var of {- (,) l n0 ->- case l of {- [] -> Prelude.Right b;- (:) y ys ->- (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))- (\_ -> Prelude.Right- b)- (\n' ->- let {filtered_var0 = f0 b __ y ys __} in- case filtered_var0 of {- Prelude.Left err -> Prelude.Left err;- Prelude.Right s ->- let {ys' = Prelude.map (f b s __) ys} in- dep_foldl_invE e s ys' n' q f f0})- n0}}
LinearScan/List1.hs view
@@ -41,6 +41,10 @@ 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 = let {
LinearScan/LiveSets.hs view
@@ -337,21 +337,18 @@ computeLocalLiveSets :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]- a1) -> a5+ a1) -> IntMap.IntMap BlockLiveSets computeLocalLiveSets maxReg mDict binfo oinfo blocks =- Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict))- Prelude.snd- (Monad.forFoldM mDict ((,) ((Prelude.succ) 0) IntMap.emptyIntMap) blocks+ Prelude.snd+ (List1.forFold ((,) ((Prelude.succ) 0) IntMap.emptyIntMap) blocks (\acc b -> case acc of { (,) idx m -> case computeLiveSets maxReg mDict binfo oinfo b idx emptyBlockLiveSets of { (,) idx' liveSets ->- Monad.bind mDict (\k ->- Applicative.pure (Monad.is_applicative mDict) ((,) idx'- (IntMap.coq_IntMap_insert k liveSets m)))- (Blocks.blockId mDict binfo b)}}))+ let {k = Blocks.blockId mDict binfo b} in+ (,) idx' (IntMap.coq_IntMap_insert k liveSets m)}})) updateLiveSets :: (IntMap.IntMap BlockLiveSets) -> ([] Blocks.BlockId) -> State.State BlockLiveSets ()@@ -380,40 +377,39 @@ computeGlobalLiveSets :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> ([] a1) -> (IntMap.IntMap- BlockLiveSets) -> a5+ BlockLiveSets) -> IntMap.IntMap BlockLiveSets computeGlobalLiveSets mDict binfo blocks liveSets =- 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 ->- case updateLiveSets liveSets suxs liveSet of {- (,) x liveSet' ->- Applicative.pure (Monad.is_applicative mDict)- (IntMap.coq_IntMap_insert bid liveSet' liveSets1)})- (Blocks.blockSuccessors mDict binfo b);- Prelude.Nothing ->- Applicative.pure (Monad.is_applicative mDict) liveSets1})- (Blocks.blockId mDict binfo b))+ List1.forFoldr liveSets blocks (\b liveSets1 ->+ let {bid = Blocks.blockId mDict binfo b} in+ case IntMap.coq_IntMap_lookup bid liveSets1 of {+ Prelude.Just liveSet ->+ let {suxs = Blocks.blockSuccessors mDict binfo b} in+ case updateLiveSets liveSets suxs liveSet of {+ (,) x liveSet' -> IntMap.coq_IntMap_insert bid liveSet' liveSets1};+ Prelude.Nothing -> liveSets1}) computeGlobalLiveSetsRecursively :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> ([] a1) ->- (IntMap.IntMap BlockLiveSets) -> a5+ (IntMap.IntMap BlockLiveSets) ->+ IntMap.IntMap BlockLiveSets computeGlobalLiveSetsRecursively mDict binfo blocks liveSets = let {- go n previous =- (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))- (\_ ->- Applicative.pure (Monad.is_applicative mDict) previous)- (\n0 ->- Monad.bind mDict (\computed ->- case Eqtype.eq_op- (IntMap.coq_IntMap_eqType coq_BlockLiveSets_eqType)- (unsafeCoerce previous) computed of {- Prelude.True ->- Applicative.pure (Monad.is_applicative mDict) computed;- Prelude.False -> unsafeCoerce go n0 computed})- (computeGlobalLiveSets mDict binfo blocks previous))- n}- in go (Data.List.length blocks) liveSets+ go = let {+ go n previous =+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ Applicative.pure Identity.coq_Identity_Applicative previous)+ (\n0 ->+ let {+ computed = computeGlobalLiveSets mDict binfo blocks previous}+ in+ case Eqtype.eq_op+ (IntMap.coq_IntMap_eqType coq_BlockLiveSets_eqType)+ (unsafeCoerce previous) (unsafeCoerce computed) of {+ Prelude.True -> unsafeCoerce computed;+ Prelude.False -> go n0 computed})+ n}+ in go}+ in+ unsafeCoerce go (Data.List.length blocks) liveSets
LinearScan/Loops.hs view
@@ -15,8 +15,8 @@ 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.Identity as Identity import qualified LinearScan.IntMap as IntMap import qualified LinearScan.IntSet as IntSet import qualified LinearScan.List1 as List1@@ -237,168 +237,149 @@ (go (IntSet.coq_IntSet_size (visitedBlocks st)) IntSet.emptyIntSet blk) computeLoopDepths :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 - a4) -> (IntMap.IntMap a1) -> State0.StateT LoopState - a5 ()+ a4) -> (IntMap.IntMap a1) -> State.State LoopState + () computeLoopDepths mDict binfo bs =- Monad.bind (State0.coq_StateT_Monad mDict) (\st ->- Monad.bind (State0.coq_StateT_Monad mDict) (\m ->- let {- f = \acc loopIndex refs ->- IntSet.coq_IntSet_forFold acc refs (\m' blk ->- let {- f = \mx ->- case mx of {- Prelude.Just y ->- case y of {- (,) idx depth -> Prelude.Just ((,) (Prelude.min idx loopIndex)- ((Prelude.succ) depth))};- Prelude.Nothing -> Prelude.Just ((,) loopIndex ((Prelude.succ)- 0))}}- in- IntMap.coq_IntMap_alter f blk m')}- in- State0.liftStateT mDict- (Monad.bind (unsafeCoerce State.coq_State_Monad) (\x ->- setLoopDepths- (IntMap.coq_IntMap_foldlWithKey f IntMap.emptyIntMap m))- (setLoopIndices m)))- (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 {- 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 (Monad.is_applicative mDict) m}))))- (State0.getT (Monad.is_applicative mDict))+ Monad.bind+ (State0.coq_StateT_Monad (unsafeCoerce Identity.coq_Identity_Monad))+ (\st ->+ let {+ m = List1.forFold IntMap.emptyIntMap+ (IntSet.coq_IntSet_toList (loopEndBlocks st)) (\m endBlock ->+ case IntMap.coq_IntMap_lookup endBlock bs of {+ Prelude.Just b ->+ let {suxs = Blocks.blockSuccessors mDict binfo b} in+ List1.forFold m (unsafeCoerce 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 {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'}});+ Prelude.Nothing -> m})}+ in+ let {+ f = \acc loopIndex refs ->+ IntSet.coq_IntSet_forFold acc refs (\m' blk ->+ let {+ f = \mx ->+ case mx of {+ Prelude.Just y ->+ case y of {+ (,) idx depth -> Prelude.Just ((,) (Prelude.min idx loopIndex)+ ((Prelude.succ) depth))};+ Prelude.Nothing -> Prelude.Just ((,) loopIndex ((Prelude.succ) 0))}}+ in+ IntMap.coq_IntMap_alter f blk m')}+ in+ State0.liftStateT (unsafeCoerce Identity.coq_Identity_Monad)+ (Monad.bind (unsafeCoerce State.coq_State_Monad) (\x ->+ setLoopDepths (IntMap.coq_IntMap_foldlWithKey f IntMap.emptyIntMap m))+ (setLoopIndices m))) (unsafeCoerce State.get) computeVarReferences :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]- a1) -> LoopState -> a5+ a1) -> LoopState -> IntMap.IntMap IntSet.IntSet computeVarReferences maxReg mDict binfo oinfo bs st =- 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))+ List1.forFold IntMap.emptyIntMap bs (\acc b ->+ let {bid = Blocks.blockId mDict binfo b} in+ 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+ IntMap.coq_IntMap_foldlWithKey g acc (loopIndices st)) findLoopEnds :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) ->- (IntMap.IntMap a1) -> State0.StateT LoopState a5 ()+ (IntMap.IntMap a1) -> State.State LoopState () findLoopEnds mDict binfo bs = let { go = let { go n b = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ ->- Applicative.pure (State0.coq_StateT_Applicative mDict) ())+ Applicative.pure State.coq_State_Applicative ()) (\n0 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\bid ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- Monad.bind (State0.coq_StateT_Monad mDict) (\suxs ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->- State0.liftStateT mDict- (modifyActiveBlocks (IntSet.coq_IntSet_delete bid)))- (Monad.forM_ (State0.coq_StateT_Monad mDict) suxs- (\sux ->- Monad.bind (State0.coq_StateT_Monad mDict) (\active ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->- Monad.bind (State0.coq_StateT_Monad mDict)- (\visited ->- case IntSet.coq_IntSet_member sux visited of {- Prelude.True ->- Applicative.pure- (State0.coq_StateT_Applicative mDict) ();- Prelude.False ->- case IntMap.coq_IntMap_lookup sux bs of {- Prelude.Just x1 -> go n0 x1;- Prelude.Nothing ->- Applicative.pure- (State0.coq_StateT_Applicative mDict) ()}})- (State0.getsT (Monad.is_applicative mDict)- visitedBlocks))- (State0.liftStateT mDict- (case IntSet.coq_IntSet_member sux active of {- Prelude.True ->- Monad.bind- (unsafeCoerce State.coq_State_Monad)- (\x0 ->- Monad.bind- (unsafeCoerce State.coq_State_Monad)- (\x1 ->- modifyBackwardBranches- (addReference sux bid))- (modifyLoopEndBlocks- (IntSet.coq_IntSet_insert bid)))- (modifyLoopHeaderBlocks (\l ->- case Prelude.not- (Ssrbool.in_mem (unsafeCoerce sux)- (Ssrbool.mem- (Seq.seq_predType- Ssrnat.nat_eqType)- (unsafeCoerce l))) of {- Prelude.True -> (:) sux l;- Prelude.False -> l}));- Prelude.False ->- modifyForwardBranches (addReference sux bid)})))- (State0.getsT (Monad.is_applicative mDict)- activeBlocks))))- (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)))))- (Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict- (State0.coq_StateT_Monad mDict)- (Blocks.blockId mDict binfo b)))+ let {bid = Blocks.blockId mDict binfo b} in+ Monad.bind State.coq_State_Monad (\x ->+ Monad.bind State.coq_State_Monad (\x0 ->+ let {suxs = Blocks.blockSuccessors mDict binfo b} in+ Monad.bind State.coq_State_Monad (\x1 ->+ unsafeCoerce+ (modifyActiveBlocks (IntSet.coq_IntSet_delete bid)))+ (Monad.forM_ State.coq_State_Monad suxs (\sux ->+ Monad.bind State.coq_State_Monad (\active ->+ Monad.bind State.coq_State_Monad (\x1 ->+ Monad.bind State.coq_State_Monad (\visited ->+ case IntSet.coq_IntSet_member sux visited of {+ Prelude.True ->+ Applicative.pure State.coq_State_Applicative ();+ Prelude.False ->+ case IntMap.coq_IntMap_lookup sux bs of {+ Prelude.Just x2 -> go n0 x2;+ Prelude.Nothing ->+ Applicative.pure State.coq_State_Applicative+ ()}})+ (State.gets (unsafeCoerce visitedBlocks)))+ (case IntSet.coq_IntSet_member sux active of {+ Prelude.True ->+ Monad.bind State.coq_State_Monad (\x1 ->+ Monad.bind State.coq_State_Monad (\x2 ->+ unsafeCoerce+ (modifyBackwardBranches+ (addReference sux bid)))+ (unsafeCoerce+ (modifyLoopEndBlocks+ (IntSet.coq_IntSet_insert bid))))+ (unsafeCoerce+ (modifyLoopHeaderBlocks (\l ->+ case Prelude.not+ (Ssrbool.in_mem (unsafeCoerce sux)+ (Ssrbool.mem+ (Seq.seq_predType+ Ssrnat.nat_eqType)+ (unsafeCoerce l))) of {+ Prelude.True -> (:) sux l;+ Prelude.False -> l})));+ Prelude.False ->+ unsafeCoerce+ (modifyForwardBranches (addReference sux bid))}))+ (State.gets (unsafeCoerce activeBlocks)))))+ (unsafeCoerce+ (modifyActiveBlocks (IntSet.coq_IntSet_insert bid))))+ (unsafeCoerce+ (modifyVisitedBlocks (IntSet.coq_IntSet_insert bid)))) n} in go} in case IntMap.coq_IntMap_toList bs of {- [] -> Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ [] -> Applicative.pure (unsafeCoerce State.coq_State_Applicative) (); (:) p l -> case p of {- (,) n b -> go (IntMap.coq_IntMap_size bs) b}}+ (,) n b -> unsafeCoerce go (IntMap.coq_IntMap_size bs) b}} computeBlockOrder :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> ([] a1) -> a5@@ -407,178 +388,142 @@ [] -> Applicative.pure (Monad.is_applicative mDict) ((,) emptyLoopState []); (:) b bs ->- Monad.bind mDict (\keys ->- let {blockMap = IntMap.coq_IntMap_fromList keys} in- Monad.bind mDict (\z ->- case z of {- (,) y st0 ->- Monad.bind mDict (\blocks' ->- Monad.bind mDict (\keys' ->- let {blockMap' = IntMap.coq_IntMap_fromList keys'} in- Monad.bind mDict (\z' ->- case z' of {- (,) y0 st1 ->- case blocks' of {- [] ->- Applicative.pure (Monad.is_applicative mDict) ((,)- emptyLoopState []);- (:) b' bs' ->- Monad.bind mDict (\w ->- case w of {- (,) y1 st2 ->- let {- isHeavier = \x y2 ->- Monad.bind mDict (\x_id ->- Monad.bind mDict (\y_id ->- let {- x_depth = case IntMap.coq_IntMap_lookup x_id- (loopDepths st2) of {- Prelude.Just p ->- case p of {- (,) idx depth -> depth};- Prelude.Nothing -> 0}}- in- let {- y_depth = case IntMap.coq_IntMap_lookup y_id- (loopDepths st2) of {- Prelude.Just p ->- case p of {- (,) idx depth -> depth};- Prelude.Nothing -> 0}}- in- Applicative.pure (Monad.is_applicative mDict)- ((Prelude.<=) ((Prelude.succ) y_depth)- x_depth)) (Blocks.blockId mDict binfo y2))- (Blocks.blockId mDict binfo x)}- in- let {- go = let {- go n branches work_list =- (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))- (\_ ->- Applicative.pure- (Monad.is_applicative mDict) [])- (\n0 ->- case work_list of {- [] ->- Applicative.pure- (Monad.is_applicative mDict) [];- (:) w0 ws ->- Monad.bind mDict (\bid ->- Monad.bind mDict (\suxs ->- Monad.bind mDict (\x ->- case x of {- (,) branches' ws' ->- Functor.fmap- (Applicative.is_functor- (Monad.is_applicative mDict))- (\x0 -> (:) w0 x0)- (go n0 branches' ws')})- (Monad.forFoldM mDict ((,)- branches ws) suxs (\acc sux ->- case acc of {- (,) branches' ws' ->- Monad.bind mDict- (\insertion ->- Applicative.pure- (Monad.is_applicative- mDict)- (case IntMap.coq_IntMap_lookup- sux branches' of {- Prelude.Just incs -> (,)- (IntMap.coq_IntMap_insert- sux- (IntSet.coq_IntSet_delete- bid incs)- branches')- (case Eqtype.eq_op- Ssrnat.nat_eqType- (unsafeCoerce- (IntSet.coq_IntSet_size- incs))- (unsafeCoerce- ((Prelude.succ)- 0)) of {- Prelude.True ->- insertion;- Prelude.False -> ws'});- Prelude.Nothing -> (,)- branches' insertion}))- (case IntMap.coq_IntMap_lookup- sux blockMap' of {- Prelude.Just s ->- Monad.insertM mDict- isHeavier s ws';- Prelude.Nothing ->- Applicative.pure- (Monad.is_applicative- mDict) ws'})})))- (Blocks.blockSuccessors mDict binfo- w0))- (Blocks.blockId mDict binfo w0)})- n}- in go}- in- Monad.bind mDict (\res ->- Applicative.pure (Monad.is_applicative mDict) ((,)- st2 res))- (go (Data.List.length blocks')- (forwardBranches st2) ((:) b' []))})- (computeLoopDepths mDict binfo blockMap st1)}})- (findLoopEnds mDict binfo blockMap' emptyLoopState))- (Monad.mapM (Monad.is_applicative mDict) (\x ->- Monad.bind mDict (\bid ->- Applicative.pure (Monad.is_applicative mDict) ((,) bid x))- (Blocks.blockId mDict binfo x)) blocks'))- (Monad.forFoldrM mDict [] blocks (\b0 rest ->- Monad.bind mDict (\suxs ->- case (Prelude.<=) (Data.List.length suxs) ((Prelude.succ) 0) of {- Prelude.True ->- Applicative.pure (Monad.is_applicative mDict) ((:) b0 rest);- Prelude.False ->- Functor.fmap- (Applicative.is_functor (Monad.is_applicative mDict))- (\x ->- case x of {- (,) b' rest' -> (:) b' rest'})- (Monad.forFoldrM mDict ((,) b0 rest) suxs (\sux x ->- case x of {- (,) b' rest' ->- let {- fsz = case IntMap.coq_IntMap_lookup sux- (forwardBranches st0) of {- Prelude.Just fwds ->- IntSet.coq_IntSet_size fwds;- Prelude.Nothing -> 0}}- in- let {- bsz = case IntMap.coq_IntMap_lookup sux- (backwardBranches st0) of {- Prelude.Just bwds ->- IntSet.coq_IntSet_size bwds;- Prelude.Nothing -> 0}}- in- case (Prelude.<=) ((Prelude.+) fsz bsz)- ((Prelude.succ) 0) of {- Prelude.True ->+ let {+ keys = Prelude.map (\x -> (,) (Blocks.blockId mDict binfo x) x) blocks}+ in+ let {blockMap = IntMap.coq_IntMap_fromList keys} in+ case findLoopEnds mDict binfo blockMap emptyLoopState of {+ (,) u st0 ->+ Monad.bind mDict (\blocks' ->+ let {+ keys' = Prelude.map (\x -> (,) (Blocks.blockId mDict binfo x) x)+ blocks'}+ in+ let {blockMap' = IntMap.coq_IntMap_fromList keys'} in+ let {z' = findLoopEnds mDict binfo blockMap' emptyLoopState} in+ case z' of {+ (,) u0 st1 ->+ case blocks' of {+ [] ->+ Applicative.pure (Monad.is_applicative mDict) ((,) emptyLoopState+ []);+ (:) b' bs' ->+ let {w = computeLoopDepths mDict binfo blockMap st1} in+ case w of {+ (,) u1 st2 ->+ let {+ isHeavier = \x y ->+ let {x_id = Blocks.blockId mDict binfo x} in+ let {y_id = Blocks.blockId mDict binfo y} in+ let {+ x_depth = case IntMap.coq_IntMap_lookup x_id+ (loopDepths st2) of {+ Prelude.Just p ->+ case p of {+ (,) idx depth -> depth};+ Prelude.Nothing -> 0}}+ in+ let {+ y_depth = case IntMap.coq_IntMap_lookup y_id+ (loopDepths st2) of {+ Prelude.Just p ->+ case p of {+ (,) idx depth -> depth};+ Prelude.Nothing -> 0}}+ in+ (Prelude.<=) ((Prelude.succ) y_depth) x_depth}+ in+ let {+ go = let {+ go n branches work_list =+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ [])+ (\n0 ->+ case work_list of {+ [] -> [];+ (:) w0 ws ->+ let {bid = Blocks.blockId mDict binfo w0} in+ let {suxs = Blocks.blockSuccessors mDict binfo w0}+ in+ let {+ x = List1.forFold ((,) branches ws) suxs+ (\acc sux ->+ case acc of {+ (,) branches' ws' ->+ let {+ insertion = case IntMap.coq_IntMap_lookup+ sux blockMap' of {+ Prelude.Just s ->+ List1.insert isHeavier s+ ws';+ Prelude.Nothing -> ws'}}+ in+ case IntMap.coq_IntMap_lookup sux+ branches' of {+ Prelude.Just incs -> (,)+ (IntMap.coq_IntMap_insert sux+ (IntSet.coq_IntSet_delete bid incs)+ branches')+ (case Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce+ (IntSet.coq_IntSet_size incs))+ (unsafeCoerce ((Prelude.succ)+ 0)) of {+ Prelude.True -> insertion;+ Prelude.False -> ws'});+ Prelude.Nothing -> (,) branches'+ insertion}})}+ in+ case x of {+ (,) branches' ws' -> (:) w0 (go n0 branches' ws')}})+ n}+ in go}+ in+ let {+ res = go (Data.List.length blocks') (forwardBranches st2) ((:)+ b' [])}+ in+ Applicative.pure (Monad.is_applicative mDict) ((,) st2 res)}}})+ (Monad.forFoldrM mDict [] blocks (\b0 rest ->+ let {suxs = Blocks.blockSuccessors mDict binfo b0} in+ case (Prelude.<=) (Data.List.length suxs) ((Prelude.succ) 0) of {+ Prelude.True ->+ Applicative.pure (Monad.is_applicative mDict) ((:) b0 rest);+ Prelude.False ->+ Functor.fmap+ (Applicative.is_functor (Monad.is_applicative mDict)) (\x ->+ case x of {+ (,) b' rest' -> (:) b' rest'})+ (Monad.forFoldrM mDict ((,) b0 rest) suxs (\sux x ->+ case x of {+ (,) b' rest' ->+ let {+ fsz = case IntMap.coq_IntMap_lookup sux+ (forwardBranches st0) of {+ Prelude.Just fwds -> IntSet.coq_IntSet_size fwds;+ Prelude.Nothing -> 0}}+ in+ let {+ bsz = case IntMap.coq_IntMap_lookup sux+ (backwardBranches st0) of {+ Prelude.Just bwds -> IntSet.coq_IntSet_size bwds;+ Prelude.Nothing -> 0}}+ in+ case (Prelude.<=) ((Prelude.+) fsz bsz) ((Prelude.succ) 0) of {+ Prelude.True ->+ Applicative.pure (Monad.is_applicative mDict) ((,) b'+ rest');+ Prelude.False ->+ case IntMap.coq_IntMap_lookup sux blockMap of {+ Prelude.Just sux' ->+ Monad.bind mDict (\z ->+ case z of {+ (,) b'' sux'' -> Applicative.pure (Monad.is_applicative mDict) ((,)- b' rest');- Prelude.False ->- case IntMap.coq_IntMap_lookup sux blockMap of {- Prelude.Just sux' ->- Monad.bind mDict (\z0 ->- case z0 of {- (,) b'' sux'' ->- Applicative.pure (Monad.is_applicative mDict)- ((,) b'' ((:) sux'' rest'))})- (Blocks.splitCriticalEdge mDict binfo b' sux');- Prelude.Nothing ->- Applicative.pure (Monad.is_applicative mDict)- ((,) b' rest')}}}))})- (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))- (Blocks.blockId mDict binfo x)) blocks)}+ b'' ((:) sux'' rest'))})+ (Blocks.splitCriticalEdge mDict binfo b' sux');+ Prelude.Nothing ->+ Applicative.pure (Monad.is_applicative mDict) ((,) b'+ rest')}}}))}))}}
LinearScan/Main.hs view
@@ -90,62 +90,64 @@ Monad.bind dict (\z -> case z of { (,) loops blocks1 ->- Monad.bind dict (\liveSets ->- Monad.bind dict (\liveSets' ->- Monad.bind dict (\ssig ->- let {- opCount = (Prelude.succ) (Blocks.countOps dict binfo blocks1)}- in- case Allocate.walkIntervals maxReg ( ssig) ((Prelude.succ)- (Ssrnat.double opCount)) of {- Prelude.Left p ->- case p of {- (,) err ssig' ->- 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' ->- case Allocate.finalizeScanState maxReg ( ssig')- (Ssrnat.double opCount) of {- Prelude.Left err ->- 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 s ->- let {allocs = Allocate.determineAllocations maxReg s} in- Monad.bind dict (\mappings ->- Monad.bind dict (\res ->- case res of {- (,) moves blocks2 ->- let {- blockInfo = case blocks2 of {- Prelude.Left vs -> Prelude.Left ((,) ((,)- (Verify.verErrors maxReg vs)- (IntMap.coq_IntMap_map (\x ->- Verify.fromRegStateDesc maxReg ( x))- (Verify.verInit maxReg vs)))- (IntMap.coq_IntMap_map (\x ->- Verify.fromRegStateDesc maxReg ( x))- (Verify.verFinal maxReg vs)));- Prelude.Right xs -> Prelude.Right xs}}- in- Applicative.pure (Monad.is_applicative dict)- (Build_Details Prelude.Nothing liveSets' moves blocks- blocks1 blockInfo (Prelude.Just- (toScanStateDescSet maxReg ( ssig))) (Prelude.Just- (toScanStateDescSet maxReg s)) 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- liveSets'))- (LiveSets.computeGlobalLiveSetsRecursively dict binfo blocks1- liveSets))- (LiveSets.computeLocalLiveSets maxReg dict binfo oinfo blocks1)})+ let {+ liveSets = LiveSets.computeLocalLiveSets maxReg dict binfo oinfo+ blocks1}+ in+ let {+ liveSets' = LiveSets.computeGlobalLiveSetsRecursively dict binfo+ blocks1 liveSets}+ in+ let {+ ssig = Build.buildIntervals maxReg dict binfo oinfo blocks1 loops+ liveSets'}+ in+ let {opCount = (Prelude.succ) (Blocks.countOps dict binfo blocks1)} in+ case Allocate.walkIntervals maxReg ( ssig) ((Prelude.succ)+ (Ssrnat.double opCount)) of {+ Prelude.Left p ->+ case p of {+ (,) err ssig' ->+ 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' ->+ case Allocate.finalizeScanState maxReg ( ssig')+ (Ssrnat.double opCount) of {+ Prelude.Left err ->+ 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 s ->+ let {allocs = Allocate.determineAllocations maxReg s} in+ let {+ mappings = Resolve.resolveDataFlow maxReg dict binfo allocs+ blocks1 liveSets'}+ in+ Monad.bind dict (\res ->+ case res of {+ (,) moves blocks2 ->+ let {+ blockInfo = case blocks2 of {+ Prelude.Left vs -> Prelude.Left ((,) ((,)+ (Verify.verErrors maxReg vs)+ (IntMap.coq_IntMap_map (\x ->+ Verify.fromRegStateDesc maxReg ( x))+ (Verify.verInit maxReg vs)))+ (IntMap.coq_IntMap_map (\x ->+ Verify.fromRegStateDesc maxReg ( x))+ (Verify.verFinal maxReg vs)));+ Prelude.Right xs -> Prelude.Right xs}}+ in+ Applicative.pure (Monad.is_applicative dict) (Build_Details+ Prelude.Nothing liveSets' moves blocks blocks1 blockInfo+ (Prelude.Just (toScanStateDescSet maxReg ( ssig)))+ (Prelude.Just (toScanStateDescSet maxReg s)) loops)})+ (Assign.assignRegNum maxReg dict binfo oinfo useVerifier allocs+ liveSets' mappings loops blocks1)}}}) (Loops.computeBlockOrder dict binfo blocks)
LinearScan/Monad.hs view
@@ -94,16 +94,3 @@ concatMapM h f l = Functor.fmap (Applicative.is_functor h) List1.concat (mapM h f l) -insertM :: (Monad a1) -> (a2 -> a2 -> a1) -> a2 -> ([] a2) -> a1-insertM h p z l =- case l of {- [] -> Applicative.pure (is_applicative h) ((:) z []);- (:) x xs ->- bind h (\b ->- case b of {- Prelude.True ->- Functor.fmap (Applicative.is_functor (is_applicative h)) (\x0 -> (:)- x x0) (insertM h p z xs);- Prelude.False ->- Applicative.pure (is_applicative h) ((:) z ((:) x xs))}) (p x z)}-
LinearScan/Resolve.hs view
@@ -14,9 +14,7 @@ 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@@ -59,8 +57,8 @@ Move PhysReg Blocks.VarId PhysReg | Spill PhysReg Blocks.VarId Prelude.Bool | Restore Blocks.VarId PhysReg Prelude.Bool- | AllocReg Blocks.VarId PhysReg Prelude.Bool- | FreeReg PhysReg Blocks.VarId Prelude.Bool+ | AllocReg Blocks.VarId PhysReg+ | FreeReg PhysReg Blocks.VarId | AssignReg Blocks.VarId PhysReg | ClearReg PhysReg Blocks.VarId | AllocStack Blocks.VarId@@ -70,19 +68,18 @@ coq_ResolvingMove_rect :: Prelude.Int -> (PhysReg -> Blocks.VarId -> PhysReg -> a1) -> (PhysReg -> Blocks.VarId -> Prelude.Bool -> a1) -> (Blocks.VarId -> PhysReg -> Prelude.Bool- -> a1) -> (Blocks.VarId -> PhysReg -> Prelude.Bool- -> a1) -> (PhysReg -> Blocks.VarId -> Prelude.Bool -> a1) -> (Blocks.VarId -> PhysReg -> a1) -> (PhysReg -> Blocks.VarId -> a1) -> (Blocks.VarId ->- a1) -> (Blocks.VarId -> a1) -> (ResolvingMove -> a1- -> a1) -> ResolvingMove -> a1+ PhysReg -> a1) -> (PhysReg -> Blocks.VarId -> a1)+ -> (Blocks.VarId -> a1) -> (Blocks.VarId -> a1) ->+ (ResolvingMove -> a1 -> a1) -> ResolvingMove -> a1 coq_ResolvingMove_rect maxReg f f0 f1 f2 f3 f4 f5 f6 f7 f8 r = case r of { Move p v p0 -> f p v p0; Spill p v b -> f0 p v b; Restore v p b -> f1 v p b;- AllocReg v p b -> f2 v p b;- FreeReg p v b -> f3 p v b;+ AllocReg v p -> f2 v p;+ FreeReg p v -> f3 p v; AssignReg v p -> f4 v p; ClearReg p v -> f5 p v; AllocStack v -> f6 v;@@ -94,8 +91,8 @@ RSMove Prelude.Int Blocks.VarId Prelude.Int | RSSpill Prelude.Int Blocks.VarId Prelude.Bool | RSRestore Blocks.VarId Prelude.Int Prelude.Bool- | RSAllocReg Blocks.VarId Prelude.Int Prelude.Bool- | RSFreeReg Prelude.Int Blocks.VarId Prelude.Bool+ | RSAllocReg Blocks.VarId Prelude.Int+ | RSFreeReg Prelude.Int Blocks.VarId | RSAssignReg Blocks.VarId Prelude.Int | RSClearReg Prelude.Int Blocks.VarId | RSAllocStack Blocks.VarId@@ -108,8 +105,8 @@ Move fr fv tr -> RSMove ( fr) fv ( tr); Spill fr tv b -> RSSpill ( fr) tv b; Restore fv tr b -> RSRestore fv ( tr) b;- AllocReg fv tr b -> RSAllocReg fv ( tr) b;- FreeReg fr tv b -> RSFreeReg ( fr) tv b;+ AllocReg fv tr -> RSAllocReg fv ( tr);+ FreeReg fr tv -> RSFreeReg ( fr) tv; AssignReg fv tr -> RSAssignReg fv ( tr); ClearReg fr tv -> RSClearReg ( fr) tv; AllocStack tv -> RSAllocStack tv;@@ -156,29 +153,23 @@ (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1) (unsafeCoerce b2))); _ -> Prelude.False};- AllocReg fv1 tr1 b1 ->+ AllocReg fv1 tr1 -> case s2 of {- AllocReg fv2 tr2 b2 ->+ AllocReg fv2 tr2 -> (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 Eqtype.bool_eqType (unsafeCoerce b1)- (unsafeCoerce b2)));+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)+ (unsafeCoerce tr2)); _ -> Prelude.False};- FreeReg fr1 tv1 b1 ->+ FreeReg fr1 tv1 -> case s2 of {- FreeReg fr2 tv2 b2 ->+ FreeReg fr2 tv2 -> (Prelude.&&) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce fr2))- ((Prelude.&&)- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1)- (unsafeCoerce tv2))- (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1)- (unsafeCoerce b2)));+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1)+ (unsafeCoerce tv2)); _ -> Prelude.False}; AssignReg fv1 tr1 -> case s2 of {@@ -294,8 +285,8 @@ in let {_evar_0_0 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_1 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_2 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_3 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_2 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_3 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_4 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_5 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \tv2 -> Ssrbool.ReflectF} in@@ -305,8 +296,8 @@ Move x x0 x1 -> unsafeCoerce _evar_0_ x x0 x1; Spill x x0 x1 -> _evar_0_0 x x0 x1; Restore x x0 x1 -> _evar_0_1 x x0 x1;- AllocReg x x0 x1 -> _evar_0_2 x x0 x1;- FreeReg x x0 x1 -> _evar_0_3 x x0 x1;+ AllocReg x x0 -> _evar_0_2 x x0;+ FreeReg x x0 -> _evar_0_3 x x0; AssignReg x x0 -> _evar_0_4 x x0; ClearReg x x0 -> _evar_0_5 x x0; AllocStack x -> _evar_0_6 x;@@ -390,8 +381,8 @@ Ssrbool.ReflectF -> _evar_0_2 __}} in let {_evar_0_2 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_3 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_4 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_3 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_4 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_5 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \tv2 -> Ssrbool.ReflectF} in@@ -401,8 +392,8 @@ Move x x0 x1 -> _evar_0_0 x x0 x1; Spill x x0 x1 -> unsafeCoerce _evar_0_1 x x0 x1; Restore x x0 x1 -> _evar_0_2 x x0 x1;- AllocReg x x0 x1 -> _evar_0_3 x x0 x1;- FreeReg x x0 x1 -> _evar_0_4 x x0 x1;+ AllocReg x x0 -> _evar_0_3 x x0;+ FreeReg x x0 -> _evar_0_4 x x0; AssignReg x x0 -> _evar_0_5 x x0; ClearReg x x0 -> _evar_0_6 x x0; AllocStack x -> _evar_0_7 x;@@ -486,8 +477,8 @@ Ssrbool.ReflectT -> _evar_0_3 __; Ssrbool.ReflectF -> _evar_0_4 __}} in- let {_evar_0_4 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_5 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_4 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_5 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_8 = \tv2 -> Ssrbool.ReflectF} in@@ -497,8 +488,8 @@ Move x x0 x1 -> _evar_0_1 x x0 x1; Spill x x0 x1 -> _evar_0_2 x x0 x1; Restore x x0 x1 -> unsafeCoerce _evar_0_3 x x0 x1;- AllocReg x x0 x1 -> _evar_0_4 x x0 x1;- FreeReg x x0 x1 -> _evar_0_5 x x0 x1;+ AllocReg x x0 -> _evar_0_4 x x0;+ FreeReg x x0 -> _evar_0_5 x x0; AssignReg x x0 -> _evar_0_6 x x0; ClearReg x x0 -> _evar_0_7 x x0; AllocStack x -> _evar_0_8 x;@@ -506,42 +497,20 @@ Looped x -> _evar_0_10 x}} in let {- _evar_0_2 = \fv1 tr1 b1 _top_assumption_0 ->+ _evar_0_2 = \fv1 tr1 _top_assumption_0 -> let {_evar_0_2 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_3 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_4 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in let {- _evar_0_5 = \fv2 tr2 b2 ->+ _evar_0_5 = \fv2 tr2 -> let { _evar_0_5 = \_ -> let { _evar_0_5 = 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 Eqtype.bool_eqType b1 b2 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 Eqtype.bool_eqType b1 b2 of {- Ssrbool.ReflectT -> _evar_0_6 __;- Ssrbool.ReflectF -> _evar_0_7 __}}+ 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 __}}@@ -551,30 +520,9 @@ let { _evar_0_6 = \_ -> let {- _evar_0_6 = \_ ->- 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 Eqtype.bool_eqType b1 b2 of {- Ssrbool.ReflectT -> _evar_0_6 __;- Ssrbool.ReflectF -> _evar_0_7 __}}- in- _evar_0_6}- in- let {- _evar_0_7 = \_ ->- let {- _evar_0_7 = \_ ->- let {_evar_0_7 = Ssrbool.ReflectF} in _evar_0_7}- in- let {_evar_0_8 = \_ -> Ssrbool.ReflectF} in- case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {- Ssrbool.ReflectT -> _evar_0_7 __;- Ssrbool.ReflectF -> _evar_0_8 __}}+ _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 __}}@@ -583,7 +531,7 @@ Ssrbool.ReflectT -> _evar_0_5 __; Ssrbool.ReflectF -> _evar_0_6 __}} in- let {_evar_0_6 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_6 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_8 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_9 = \tv2 -> Ssrbool.ReflectF} in@@ -593,8 +541,8 @@ Move x x0 x1 -> _evar_0_2 x x0 x1; Spill x x0 x1 -> _evar_0_3 x x0 x1; Restore x x0 x1 -> _evar_0_4 x x0 x1;- AllocReg x x0 x1 -> unsafeCoerce _evar_0_5 x x0 x1;- FreeReg x x0 x1 -> _evar_0_6 x x0 x1;+ AllocReg x x0 -> unsafeCoerce _evar_0_5 x x0;+ FreeReg x x0 -> _evar_0_6 x x0; AssignReg x x0 -> _evar_0_7 x x0; ClearReg x x0 -> _evar_0_8 x x0; AllocStack x -> _evar_0_9 x;@@ -602,43 +550,21 @@ Looped x -> _evar_0_11 x}} in let {- _evar_0_3 = \fr1 tv1 b1 _top_assumption_0 ->+ _evar_0_3 = \fr1 tv1 _top_assumption_0 -> let {_evar_0_3 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_4 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_5 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_6 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_6 = \fv2 tr2 -> Ssrbool.ReflectF} in let {- _evar_0_7 = \fr2 tv2 b2 ->+ _evar_0_7 = \fr2 tv2 -> let { _evar_0_7 = \_ -> let { _evar_0_7 = 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 Eqtype.bool_eqType b1 b2 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 Eqtype.bool_eqType b1 b2 of {- Ssrbool.ReflectT -> _evar_0_8 __;- Ssrbool.ReflectF -> _evar_0_9 __}}+ let {_evar_0_7 = Ssrbool.ReflectT} in _evar_0_7} in+ let {_evar_0_8 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_7 __; Ssrbool.ReflectF -> _evar_0_8 __}}@@ -648,30 +574,9 @@ let { _evar_0_8 = \_ -> let {- _evar_0_8 = \_ ->- 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 Eqtype.bool_eqType b1 b2 of {- Ssrbool.ReflectT -> _evar_0_8 __;- Ssrbool.ReflectF -> _evar_0_9 __}}- in- _evar_0_8}- in- let {- _evar_0_9 = \_ ->- let {- _evar_0_9 = \_ ->- let {_evar_0_9 = Ssrbool.ReflectF} in _evar_0_9}- in- let {_evar_0_10 = \_ -> Ssrbool.ReflectF} in- case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {- Ssrbool.ReflectT -> _evar_0_9 __;- Ssrbool.ReflectF -> _evar_0_10 __}}+ _evar_0_8 = \_ -> let {_evar_0_8 = Ssrbool.ReflectF} in _evar_0_8} in+ let {_evar_0_9 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_8 __; Ssrbool.ReflectF -> _evar_0_9 __}}@@ -689,8 +594,8 @@ Move x x0 x1 -> _evar_0_3 x x0 x1; Spill x x0 x1 -> _evar_0_4 x x0 x1; Restore x x0 x1 -> _evar_0_5 x x0 x1;- AllocReg x x0 x1 -> _evar_0_6 x x0 x1;- FreeReg x x0 x1 -> unsafeCoerce _evar_0_7 x x0 x1;+ AllocReg x x0 -> _evar_0_6 x x0;+ FreeReg x x0 -> unsafeCoerce _evar_0_7 x x0; AssignReg x x0 -> _evar_0_8 x x0; ClearReg x x0 -> _evar_0_9 x x0; AllocStack x -> _evar_0_10 x;@@ -702,8 +607,8 @@ let {_evar_0_4 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_5 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_7 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_8 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_7 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_8 = \fr2 tv2 -> Ssrbool.ReflectF} in let { _evar_0_9 = \fr2 tv2 -> let {@@ -743,8 +648,8 @@ Move x x0 x1 -> _evar_0_4 x x0 x1; Spill x x0 x1 -> _evar_0_5 x x0 x1; Restore x x0 x1 -> _evar_0_6 x x0 x1;- AllocReg x x0 x1 -> _evar_0_7 x x0 x1;- FreeReg x x0 x1 -> _evar_0_8 x x0 x1;+ AllocReg x x0 -> _evar_0_7 x x0;+ FreeReg x x0 -> _evar_0_8 x x0; AssignReg x x0 -> unsafeCoerce _evar_0_9 x x0; ClearReg x x0 -> _evar_0_10 x x0; AllocStack x -> _evar_0_11 x;@@ -756,8 +661,8 @@ let {_evar_0_5 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_8 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_9 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_8 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_9 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_10 = \fr2 tv2 -> Ssrbool.ReflectF} in let { _evar_0_11 = \fr2 tv2 ->@@ -797,8 +702,8 @@ Move x x0 x1 -> _evar_0_5 x x0 x1; Spill x x0 x1 -> _evar_0_6 x x0 x1; Restore x x0 x1 -> _evar_0_7 x x0 x1;- AllocReg x x0 x1 -> _evar_0_8 x x0 x1;- FreeReg x x0 x1 -> _evar_0_9 x x0 x1;+ AllocReg x x0 -> _evar_0_8 x x0;+ FreeReg x x0 -> _evar_0_9 x x0; AssignReg x x0 -> _evar_0_10 x x0; ClearReg x x0 -> unsafeCoerce _evar_0_11 x x0; AllocStack x -> _evar_0_12 x;@@ -810,8 +715,8 @@ let {_evar_0_6 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_8 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_9 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_10 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_9 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_10 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_11 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_12 = \fr2 tv2 -> Ssrbool.ReflectF} in let {@@ -830,8 +735,8 @@ Move x x0 x1 -> _evar_0_6 x x0 x1; Spill x x0 x1 -> _evar_0_7 x x0 x1; Restore x x0 x1 -> _evar_0_8 x x0 x1;- AllocReg x x0 x1 -> _evar_0_9 x x0 x1;- FreeReg x x0 x1 -> _evar_0_10 x x0 x1;+ AllocReg x x0 -> _evar_0_9 x x0;+ FreeReg x x0 -> _evar_0_10 x x0; AssignReg x x0 -> _evar_0_11 x x0; ClearReg x x0 -> _evar_0_12 x x0; AllocStack x -> unsafeCoerce _evar_0_13 x;@@ -843,8 +748,8 @@ let {_evar_0_7 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_8 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_9 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_10 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_11 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_10 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_11 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_12 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_13 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_14 = \tv2 -> Ssrbool.ReflectF} in@@ -863,8 +768,8 @@ Move x x0 x1 -> _evar_0_7 x x0 x1; Spill x x0 x1 -> _evar_0_8 x x0 x1; Restore x x0 x1 -> _evar_0_9 x x0 x1;- AllocReg x x0 x1 -> _evar_0_10 x x0 x1;- FreeReg x x0 x1 -> _evar_0_11 x x0 x1;+ AllocReg x x0 -> _evar_0_10 x x0;+ FreeReg x x0 -> _evar_0_11 x x0; AssignReg x x0 -> _evar_0_12 x x0; ClearReg x x0 -> _evar_0_13 x x0; AllocStack x -> _evar_0_14 x;@@ -876,8 +781,8 @@ let {_evar_0_8 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_9 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_10 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_11 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in- let {_evar_0_12 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_11 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_12 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_13 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_14 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_15 = \tv2 -> Ssrbool.ReflectF} in@@ -895,8 +800,8 @@ Move x0 x1 x2 -> _evar_0_8 x0 x1 x2; Spill x0 x1 x2 -> _evar_0_9 x0 x1 x2; Restore x0 x1 x2 -> _evar_0_10 x0 x1 x2;- AllocReg x0 x1 x2 -> _evar_0_11 x0 x1 x2;- FreeReg x0 x1 x2 -> _evar_0_12 x0 x1 x2;+ AllocReg x0 x1 -> _evar_0_11 x0 x1;+ FreeReg x0 x1 -> _evar_0_12 x0 x1; AssignReg x0 x1 -> _evar_0_13 x0 x1; ClearReg x0 x1 -> _evar_0_14 x0 x1; AllocStack x0 -> _evar_0_15 x0;@@ -919,9 +824,9 @@ coq_ResolvingMove_eqType maxReg = unsafeCoerce (coq_ResolvingMove_eqMixin maxReg) -addResolvingEdge :: Prelude.Int -> ResolvingMove -> ResolvingMove ->- Prelude.Bool-addResolvingEdge maxReg x y =+shouldAddResolvingEdge :: Prelude.Int -> ResolvingMove -> ResolvingMove ->+ Prelude.Bool+shouldAddResolvingEdge maxReg x y = case x of { Move fr1 fv1 tr1 -> case y of {@@ -937,7 +842,7 @@ Restore v tr2 b -> Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce tr2);- FreeReg fr2 tv2 b ->+ FreeReg fr2 tv2 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce tv2))@@ -955,10 +860,10 @@ Restore v tr2 b0 -> Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce tr2);- AllocReg v tr2 b0 ->+ AllocReg v tr2 -> Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce tr2);- FreeReg fr2 tv2 b0 ->+ FreeReg fr2 tv2 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce tv2))@@ -988,7 +893,7 @@ FreeStack fv2 -> Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce fv2); _ -> Prelude.False};- AllocReg fv2 tr2 b ->+ AllocReg fv2 tr2 -> case y of { Move p fv3 tr3 -> (Prelude.&&)@@ -996,25 +901,25 @@ (unsafeCoerce fv3)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr2) (unsafeCoerce tr3));- Restore tv2 tr3 b0 ->+ Restore tv2 tr3 b -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv2) (unsafeCoerce tv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr2) (unsafeCoerce tr3));- FreeReg fr1 tv1 b0 ->+ FreeReg fr1 tv1 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce fv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce tr2)); _ -> Prelude.False};- FreeReg fr1 v b ->+ FreeReg fr1 v -> case y of {- Restore v0 tr2 b0 ->+ Restore v0 tr2 b -> Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce tr2);- AllocReg v0 tr2 b0 ->+ AllocReg v0 tr2 -> Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce tr2); _ -> Prelude.False};@@ -1029,7 +934,7 @@ addResolution maxReg x g = let { f = \x0 y z ->- case addResolvingEdge maxReg x0 y of {+ case shouldAddResolvingEdge maxReg x0 y of { Prelude.True -> Graph.addEdge (coq_ResolvingMove_eqType maxReg) (unsafeCoerce ((,) x0 y)) z;@@ -1101,35 +1006,31 @@ Prelude.Just yr -> Prelude.Just (case (Prelude.||) (varNotLive vid) (Prelude.not (Ssrnat.odd to)) of {- Prelude.True -> (:) (FreeReg xr vid Prelude.True) ((:)- (AllocReg vid yr Prelude.True) []);- Prelude.False -> (:) (FreeReg xr vid Prelude.False) ((:)- (AllocReg vid yr Prelude.False) ((:) (Move xr vid yr) ((:)- (AssignReg vid yr) [])))});- Prelude.Nothing -> Prelude.Just ((:) (FreeReg xr vid- Prelude.False) ((:) (AllocStack vid) ((:) (Spill xr vid- Prelude.False) [])))};+ Prelude.True -> (:) (FreeReg xr vid) ((:) (AllocReg vid yr)+ []);+ Prelude.False -> (:) (FreeReg xr vid) ((:) (AllocReg vid yr)+ ((:) (Move xr vid yr) ((:) (AssignReg vid yr) [])))});+ Prelude.Nothing -> Prelude.Just ((:) (FreeReg xr vid) ((:)+ (AllocStack vid) ((:) (Spill xr vid Prelude.False) [])))}; Prelude.Nothing -> case Allocate.intReg maxReg y of { Prelude.Just yr -> Prelude.Just (case (Prelude.||) (varNotLive vid) (Prelude.not (Ssrnat.odd to)) of {- Prelude.True -> (:) (AllocReg vid yr Prelude.False) [];- Prelude.False -> (:) (AllocReg vid yr Prelude.False) ((:)- (Restore vid yr Prelude.False) ((:) (AssignReg vid yr) ((:)- (FreeStack vid) [])))});+ Prelude.True -> (:) (AllocReg vid yr) [];+ Prelude.False -> (:) (AllocReg vid yr) ((:) (Restore vid yr+ Prelude.False) ((:) (AssignReg vid yr) ((:) (FreeStack vid)+ [])))}); Prelude.Nothing -> Prelude.Nothing}}}; Prelude.Nothing -> case Allocate.intReg maxReg x of {- Prelude.Just r -> Prelude.Just ((:) (FreeReg r vid Prelude.False)- []);+ Prelude.Just r -> Prelude.Just ((:) (FreeReg r vid) []); Prelude.Nothing -> Prelude.Just ((:) (FreeStack vid) [])}}; Prelude.Nothing -> case my of { Prelude.Just y -> case Allocate.intReg maxReg y of {- Prelude.Just r -> Prelude.Just ((:) (AllocReg vid r Prelude.False)- []);+ Prelude.Just r -> Prelude.Just ((:) (AllocReg vid r) []); Prelude.Nothing -> Prelude.Just ((:) (AllocStack vid) [])}; Prelude.Nothing -> Prelude.Nothing}}) (allocsAt from) (allocsAt to) @@ -1172,52 +1073,47 @@ resolveDataFlow :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> ([] Allocate.Allocation) -> ([] - a1) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> a5+ a1) -> (IntMap.IntMap LiveSets.BlockLiveSets) ->+ IntMap.IntMap BlockMoves 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 ->+ Prelude.fst+ (List1.forFold ((,) 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 ->- checkBlockBoundary maxReg allocs- (LiveSets.blockLiveIn from) bid Prelude.False- Prelude.Nothing from mappings;- 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 -> mappings';- 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- (LiveSets.blockLiveIn to) key in_from- (Prelude.Just from) 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)}))+ let {bid = Blocks.blockId mDict binfo b} in+ case IntMap.coq_IntMap_lookup bid liveSets of {+ Prelude.Just from ->+ let {+ mappings' = case isFirst of {+ Prelude.True ->+ checkBlockBoundary maxReg allocs+ (LiveSets.blockLiveIn from) bid Prelude.False+ Prelude.Nothing from mappings;+ Prelude.False -> mappings}}+ in+ let {suxs = Blocks.blockSuccessors mDict binfo b} in+ 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 -> mappings';+ 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+ (LiveSets.blockLiveIn to) key in_from+ (Prelude.Just from) to ms;+ Prelude.Nothing -> ms})}}+ in+ (,) mappings'' Prelude.False;+ Prelude.Nothing -> (,) mappings Prelude.False}}))
LinearScan/State.hs view
@@ -54,6 +54,10 @@ get i = (,) i i +gets :: (a1 -> a2) -> State a1 a2+gets f s =+ (,) (f s) s+ modify :: (a1 -> a1) -> State a1 () modify f i = (,) () (f i)
LinearScan/State0.hs view
@@ -45,10 +45,6 @@ getT h i = Applicative.pure h ((,) i i) -getsT :: (Applicative.Applicative a1) -> (a2 -> a3) -> StateT a2 a1 a3-getsT h f s =- Applicative.pure h ((,) (f s) s)- putT :: (Applicative.Applicative a1) -> a2 -> StateT a2 a1 () putT h x x0 = Applicative.pure h ((,) () x)
LinearScan/UsePos.hs view
@@ -145,9 +145,9 @@ case u of { Build_UsePos uloc0 regReq0 uvar0 -> uvar0} -upos_le :: UsePos -> UsePos -> Prelude.Bool-upos_le x y =- (Prelude.<=) (uloc x) (uloc y)+upos_le :: Ssrbool.Coq_rel UsePos+upos_le m n =+ (Prelude.<=) (uloc m) (uloc n) head_or :: Prelude.Int -> ([] UsePos) -> Prelude.Int head_or x xs =
LinearScan/Verify.hs view
@@ -302,8 +302,8 @@ Prelude.False -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()} reserveReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->- Blocks.VarId -> Prelude.Bool -> Verified a1 a2 ()-reserveReg maxReg mDict pc reg var fromSplit =+ 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@@ -330,7 +330,7 @@ Prelude.Nothing -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))- (addMove maxReg mDict pc (Resolve.RSAllocReg var ( reg) fromSplit))+ (addMove maxReg mDict pc (Resolve.RSAllocReg var ( reg))) isReserved :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Verified a1 a2 (Prelude.Maybe Blocks.VarId)@@ -360,8 +360,8 @@ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) releaseReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->- Blocks.VarId -> Prelude.Bool -> Verified a1 a2 ()-releaseReg maxReg mDict pc reg var fromSplit =+ 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@@ -382,7 +382,7 @@ (Vector0.vnth maxReg (rsAllocs maxReg st) reg)) ((Prelude.succ) ((Prelude.succ) 0)))}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))- (addMove maxReg mDict pc (Resolve.RSFreeReg ( reg) var fromSplit))+ (addMove maxReg mDict pc (Resolve.RSFreeReg ( reg) var)) clearReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier -> PhysReg -> Blocks.VarId -> Verified a1 a2 ()@@ -676,9 +676,11 @@ UsePos.Input -> checkResidency maxReg mDict pc useVerifier reg var; UsePos.InputOutput -> Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- checkAllocation maxReg mDict pc intervals (Prelude.Just- (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ) 0))- (checkResidency maxReg mDict pc useVerifier reg var);+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ assignReg maxReg mDict pc useVerifier reg var)+ (checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)+ 0))) (checkResidency maxReg mDict pc useVerifier reg var); UsePos.Temp -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> checkReservation maxReg mDict pc reg var)@@ -733,9 +735,11 @@ UsePos.Input -> checkResidency maxReg mDict pc useVerifier reg var; UsePos.InputOutput -> Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- checkAllocation maxReg mDict pc intervals (Prelude.Just- (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ) 0))- (checkResidency maxReg mDict pc useVerifier reg var);+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ assignReg maxReg mDict pc useVerifier reg var)+ (checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)+ 0))) (checkResidency maxReg mDict pc useVerifier reg var); UsePos.Temp -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> checkReservation maxReg mDict pc reg var)@@ -801,14 +805,14 @@ (Resolve.weakenResolvingMove maxReg mv))) (checkReservation maxReg mDict pc toReg fromSpillSlot)) (checkStack maxReg mDict pc useVerifier fromSpillSlot);- Resolve.AllocReg toVar toReg fromSplit ->+ Resolve.AllocReg toVar toReg -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc)- (reserveReg maxReg mDict pc toReg toVar fromSplit);- Resolve.FreeReg fromReg fromVar fromSplit ->+ (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 fromSplit);+ (releaseReg maxReg mDict pc fromReg fromVar); Resolve.AssignReg fromVar toReg -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc)@@ -881,13 +885,13 @@ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0))))))))));- Resolve.AllocReg toVar toReg fromSplit ->+ Resolve.AllocReg toVar toReg -> checkAllocation maxReg mDict pc intervals (Prelude.Just (Prelude.Just toReg)) toVar to ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0))))))))));- Resolve.FreeReg fromReg fromVar fromSplit ->+ Resolve.FreeReg fromReg fromVar -> checkAllocation maxReg mDict pc intervals (Prelude.Just (Prelude.Just fromReg)) fromVar from ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
linearscan.cabal view
@@ -1,5 +1,5 @@ name: linearscan-version: 0.10.2+version: 0.11 synopsis: Linear scan register allocator, formally verified in Coq homepage: http://github.com/jwiegley/linearscan license: BSD3