diff --git a/LinearScan.hs b/LinearScan.hs --- a/LinearScan.hs +++ b/LinearScan.hs @@ -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) = - " (r" ++ show tr ++ " v" ++ show fv ++ ")" ++ showSplit b - show (LS.RSFreeReg fr tv b) = - " (r" ++ show fr ++ " v" ++ show tv ++ ")" ++ showSplit b + show (LS.RSAllocReg fv tr) = + " (r" ++ show tr ++ " v" ++ show fv ++ ")" + show (LS.RSFreeReg fr tv) = + " (r" ++ show fr ++ " v" ++ show tv ++ ")" show (LS.RSAssignReg fv tr) = " (r" ++ show tr ++ " v" ++ show fv ++ ")" show (LS.RSClearReg fr tv) = diff --git a/LinearScan/Allocate.hs b/LinearScan/Allocate.hs --- a/LinearScan/Allocate.hs +++ b/LinearScan/Allocate.hs @@ -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 diff --git a/LinearScan/Assign.hs b/LinearScan/Assign.hs --- a/LinearScan/Assign.hs +++ b/LinearScan/Assign.hs @@ -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 diff --git a/LinearScan/Blocks.hs b/LinearScan/Blocks.hs --- a/LinearScan/Blocks.hs +++ b/LinearScan/Blocks.hs @@ -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 diff --git a/LinearScan/Build.hs b/LinearScan/Build.hs --- a/LinearScan/Build.hs +++ b/LinearScan/Build.hs @@ -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)}} diff --git a/LinearScan/Lib.hs b/LinearScan/Lib.hs --- a/LinearScan/Lib.hs +++ b/LinearScan/Lib.hs @@ -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}} diff --git a/LinearScan/List1.hs b/LinearScan/List1.hs --- a/LinearScan/List1.hs +++ b/LinearScan/List1.hs @@ -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 { diff --git a/LinearScan/LiveSets.hs b/LinearScan/LiveSets.hs --- a/LinearScan/LiveSets.hs +++ b/LinearScan/LiveSets.hs @@ -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 diff --git a/LinearScan/Loops.hs b/LinearScan/Loops.hs --- a/LinearScan/Loops.hs +++ b/LinearScan/Loops.hs @@ -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')}}}))}))}} diff --git a/LinearScan/Main.hs b/LinearScan/Main.hs --- a/LinearScan/Main.hs +++ b/LinearScan/Main.hs @@ -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) diff --git a/LinearScan/Monad.hs b/LinearScan/Monad.hs --- a/LinearScan/Monad.hs +++ b/LinearScan/Monad.hs @@ -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)} - diff --git a/LinearScan/Resolve.hs b/LinearScan/Resolve.hs --- a/LinearScan/Resolve.hs +++ b/LinearScan/Resolve.hs @@ -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}})) diff --git a/LinearScan/State.hs b/LinearScan/State.hs --- a/LinearScan/State.hs +++ b/LinearScan/State.hs @@ -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) diff --git a/LinearScan/State0.hs b/LinearScan/State0.hs --- a/LinearScan/State0.hs +++ b/LinearScan/State0.hs @@ -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) diff --git a/LinearScan/UsePos.hs b/LinearScan/UsePos.hs --- a/LinearScan/UsePos.hs +++ b/LinearScan/UsePos.hs @@ -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 = diff --git a/LinearScan/Verify.hs b/LinearScan/Verify.hs --- a/LinearScan/Verify.hs +++ b/LinearScan/Verify.hs @@ -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) diff --git a/linearscan.cabal b/linearscan.cabal --- a/linearscan.cabal +++ b/linearscan.cabal @@ -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