linearscan 0.11 → 0.11.1
raw patch · 16 files changed
+163/−108 lines, 16 files
Files
- LinearScan/Allocate.hs +14/−14
- LinearScan/Blocks.hs +1/−1
- LinearScan/Build.hs +11/−9
- LinearScan/Contravariant.hs +37/−0
- LinearScan/Fintype.hs +4/−2
- LinearScan/Interval.hs +3/−2
- LinearScan/List1.hs +3/−4
- LinearScan/Main.hs +7/−7
- LinearScan/Monad.hs +2/−2
- LinearScan/Morph.hs +2/−2
- LinearScan/Resolve.hs +7/−7
- LinearScan/Seq.hs +4/−0
- LinearScan/Spill.hs +20/−16
- LinearScan/Split.hs +22/−20
- LinearScan/Verify.hs +22/−17
- linearscan.cabal +4/−5
LinearScan/Allocate.hs view
@@ -142,8 +142,8 @@ (Morph.moveUnhandledToActive maxReg pre reg)} in let {cid = Cursor.curId maxReg sd} in- Context.context (Trace.ETryAllocateFreeReg ( reg) mres- ( (Prelude.fst cid)))+ Context.context (Trace.ETryAllocateFreeReg (Prelude.id reg) mres+ (Prelude.id (Prelude.fst cid))) (Context.ipure (case mres of { Prelude.Just n ->@@ -211,8 +211,8 @@ nextUsePos'' of { (,) reg mres -> let {cid = Cursor.curId maxReg sd} in- Context.context (Trace.EAllocateBlockedReg ( reg) mres- ( (Prelude.fst cid)))+ Context.context (Trace.EAllocateBlockedReg (Prelude.id reg) mres+ (Prelude.id (Prelude.fst cid))) (case case mres of { Prelude.Just n -> (Prelude.<=) ((Prelude.succ) n)@@ -236,7 +236,7 @@ (case mloc of { Prelude.Just n -> Context.context (Trace.EIntersectsWithFixedInterval n- ( reg))+ (Prelude.id reg)) (Split.splitCurrentInterval maxReg pre (Split.BeforePos n)); Prelude.Nothing -> Context.ipure ()}))@@ -247,8 +247,8 @@ morphlen_transport :: Prelude.Int -> ScanState.ScanStateDesc -> ScanState.ScanStateDesc -> ScanState.IntervalId -> ScanState.IntervalId-morphlen_transport maxReg b b' = GHC.Base.id- +morphlen_transport maxReg b b' =+ Prelude.id mt_fst :: Prelude.Int -> ScanState.ScanStateDesc -> ScanState.ScanStateDesc -> ((,) ScanState.IntervalId PhysReg) -> (,) ScanState.IntervalId@@ -291,8 +291,8 @@ in Prelude.Right filtered_var0; Prelude.Nothing -> Prelude.Left ((:)- (Trace.ERegisterAssignmentsOverlap ( (Prelude.snd x))- ( (Prelude.fst x)) ((Prelude.succ) 0)) e)};+ (Trace.ERegisterAssignmentsOverlap (Prelude.id (Prelude.snd x))+ (Prelude.id (Prelude.fst x)) ((Prelude.succ) 0)) e)}; Prelude.False -> Prelude.Right (case Prelude.not (Interval.posWithinInterval@@ -378,8 +378,8 @@ in Prelude.Right filtered_var0; Prelude.False -> Prelude.Left ((:) (Trace.ERegisterAssignmentsOverlap- ( (Prelude.snd x)) ( (Prelude.fst x)) ((Prelude.succ) ((Prelude.succ)- 0))) e)}+ (Prelude.id (Prelude.snd x)) (Prelude.id (Prelude.fst x)) ((Prelude.succ)+ ((Prelude.succ) 0))) e)} goInactive :: Prelude.Int -> Prelude.Int -> ScanState.ScanStateDesc -> ([] Trace.SSTrace) -> ScanState.ScanStateDesc -> ((,)@@ -410,8 +410,8 @@ in f filtered_var0; Prelude.Nothing -> Prelude.Left ((:) (Trace.ERegisterAssignmentsOverlap- ( (Prelude.snd x)) ( (Prelude.fst x)) ((Prelude.succ) ((Prelude.succ)- ((Prelude.succ) 0)))) e)};+ (Prelude.id (Prelude.snd x)) (Prelude.id (Prelude.fst x))+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0)))) e)}; Prelude.False -> case Interval.posWithinInterval (@@ -596,7 +596,7 @@ determineAllocations :: Prelude.Int -> ScanState.ScanStateDesc -> [] Allocation determineAllocations maxReg sd =- Prelude.map (\x -> Build_Allocation ( (Prelude.fst x))+ Prelude.map (\x -> Build_Allocation (Prelude.id (Prelude.fst x)) (Interval.getIntervalDesc ( (Vector0.vnth (ScanState.nextInterval maxReg sd)
LinearScan/Blocks.hs view
@@ -41,7 +41,7 @@ nat_of_varId :: Prelude.Int -> VarInfo -> Prelude.Int nat_of_varId maxReg v = case varId maxReg v of {- Prelude.Left n -> n;+ Prelude.Left n -> Prelude.id n; Prelude.Right v0 -> (Prelude.+) v0 maxReg} data OpKind =
LinearScan/Build.hs view
@@ -144,7 +144,8 @@ let { _top_assumption_ = compilePendingRanges b e (List1.insert (coq_BoundedRange_leq b e) r- (List1.sortBy (coq_BoundedRange_leq b e) ( rs)))}+ (List1.sortBy (coq_BoundedRange_leq b e)+ (Prelude.id rs)))} in let { _evar_0_0 = \_ _ ->@@ -158,7 +159,7 @@ (:) y ys -> rangesToBoundedRanges b e y ys}} in case List1.insert (coq_BoundedRange_leq b e) r- (List1.sortBy (coq_BoundedRange_leq b e) ( rs)) of {+ (List1.sortBy (coq_BoundedRange_leq b e) (Prelude.id rs)) of { [] -> _evar_0_0 __ __; (:) x x0 -> _evar_0_1 x x0}} in@@ -178,14 +179,15 @@ IntMap.coq_IntMap_mergeWithKey (\_the_1st_wildcard_ brs srs2 -> let { _top_assumption_ = compilePendingRanges b e- (List1.sortBy (coq_BoundedRange_leq b e) ( brs))}+ (List1.sortBy (coq_BoundedRange_leq b e)+ (Prelude.id brs))} in Prelude.Just (Range.coq_SortedRanges_cat ((Prelude.succ) (Ssrnat.double b)) _top_assumption_ ((Prelude.succ) (Ssrnat.double e)) srs2)) (IntMap.coq_IntMap_map (\brs -> compilePendingRanges b e- (List1.sortBy (coq_BoundedRange_leq b e) ( brs)))) (\sr ->+ (List1.sortBy (coq_BoundedRange_leq b e) (Prelude.id brs)))) (\sr -> (Prelude.flip (Prelude.$)) __ (\_ -> IntMap.coq_IntMap_map (Range.transportSortedRanges ((Prelude.succ) (Ssrnat.double b))@@ -297,7 +299,7 @@ in let { _evar_0_0 = \_the_2nd_wildcard_ rs -> Prelude.Just- (NonEmpty.coq_NE_from_list br ( rs))}+ (NonEmpty.coq_NE_from_list br (Prelude.id rs))} in (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs) (\x ->@@ -309,7 +311,7 @@ let { _evar_0_0 = (Prelude.flip (Prelude.$)) _top_assumption_0 (\br -> Prelude.Just- (NonEmpty.coq_NE_from_list br ( range0)))}+ (NonEmpty.coq_NE_from_list br (Prelude.id range0)))} in case replaceFirst of { Prelude.True -> _evar_0_;@@ -318,7 +320,7 @@ let { _evar_0_0 = \_ -> Prelude.Just (NonEmpty.coq_NE_from_list (makeNewRange b pos e _top_assumption_)- ( range0))}+ (Prelude.id range0))} in case upos_before_rend ( _top_assumption_0) _top_assumption_ of { Prelude.True -> _evar_0_ __;@@ -342,7 +344,7 @@ let { _evar_0_ = \range0 -> Prelude.Just (NonEmpty.coq_NE_from_list (makeNewRange b pos e _top_assumption_)- ( range0))}+ (Prelude.id range0))} in let { _evar_0_0 = Prelude.Just ((:[]) (makeNewRange b pos e _top_assumption_))}@@ -405,7 +407,7 @@ IntMap.IntMap PendingRanges handleVars maxReg varRefs b pos e ranges = let {- vars = Prelude.id + vars = IntMap.coq_IntMap_map Prelude.id (IntMap.coq_IntMap_groupOn (Blocks.nat_of_varId maxReg) varRefs)} in IntMap.coq_IntMap_mergeWithKey (handleVars_combine maxReg b pos e)
+ LinearScan/Contravariant.hs view
@@ -0,0 +1,37 @@+{-# OPTIONS_GHC -cpp -XMagicHash #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Contravariant where+++import Debug.Trace (trace, traceShow, traceShowId)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified Hask.Utils++++#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+import qualified GHC.Prim as GHC.Prim+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+#endif+++#ifdef __GLASGOW_HASKELL__+type Any = GHC.Prim.Any+#else+-- HUGS+type Any = ()+#endif++type Contravariant f =+ () -> () -> (Any -> Any) -> f -> f+ -- singleton inductive, whose constructor was Build_Contravariant+
LinearScan/Fintype.hs view
@@ -107,14 +107,16 @@ ordinal_subType :: Prelude.Int -> Eqtype.Coq_subType Prelude.Int ordinal_subType n =- Eqtype.SubType (unsafeCoerce ) (unsafeCoerce (\x _ -> x)) (\_ k_S u ->+ Eqtype.SubType (unsafeCoerce Prelude.id) (unsafeCoerce (\x _ -> x))+ (\_ k_S u -> case unsafeCoerce u of { x -> k_S x __}) ordinal_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of Prelude.Int ordinal_eqMixin n = Eqtype.Equality__Mixin (\x y ->- Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce ( x)) (unsafeCoerce ( y)))+ Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Prelude.id x))+ (unsafeCoerce (Prelude.id y))) (unsafeCoerce (Eqtype.val_eqP Ssrnat.nat_eqType (\x -> (Prelude.<=) ((Prelude.succ) (unsafeCoerce x)) n)
LinearScan/Interval.hs view
@@ -200,7 +200,7 @@ Prelude.True -> Range.rbeg ( r); Prelude.False -> ibeg x}); Prelude.False -> go rs0}}}- in go ( (rds y))+ in go (Prelude.id (rds y)) divideIntervalRanges :: IntervalDesc -> Prelude.Int -> ((,) Range.SortedRanges Range.SortedRanges)@@ -328,7 +328,8 @@ [] -> _evar_0_; (:) x x0 -> _evar_0_0 x x0}} in- case List1.span (\rd -> (Prelude.<=) (Range.rend ( rd)) before) ( (rds d)) of {+ case List1.span (\rd -> (Prelude.<=) (Range.rend ( rd)) before)+ (Prelude.id (rds d)) of { (,) x x0 -> _evar_0_ x x0 __} splitIntervalRanges :: IntervalDesc -> Prelude.Int ->
LinearScan/List1.hs view
@@ -13,16 +13,15 @@ import qualified Hask.Utils import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Seq as Seq __ :: any __ = Prelude.error "Logical or arity value used" concat :: ([] ([] a1)) -> [] a1-concat l =- case l of {- [] -> [];- (:) x xs -> (Prelude.++) x (concat xs)}+concat =+ Seq.flatten maybeLookup :: Eqtype.Equality__Coq_type -> ([] ((,) Eqtype.Equality__Coq_sort a1)) ->
LinearScan/Main.hs view
@@ -56,14 +56,14 @@ Prelude.Just x -> Prelude.Just (Interval.getIntervalDesc ( x)); Prelude.Nothing -> Prelude.Nothing}) (Vector0.vec_to_seq maxReg (ScanState.fixedIntervals maxReg sd)))- (Prelude.map (\i -> (,) ( (Prelude.fst i)) (Prelude.snd i))+ (Prelude.map (\i -> (,) (Prelude.id (Prelude.fst i)) (Prelude.snd i)) (ScanState.unhandled maxReg sd))- (Prelude.map (\i -> (,) ( (Prelude.fst i)) ( (Prelude.snd i)))- (ScanState.active maxReg sd))- (Prelude.map (\i -> (,) ( (Prelude.fst i)) ( (Prelude.snd i)))- (ScanState.inactive maxReg sd))- (Prelude.map (\i -> (,) ( (Prelude.fst i))- (Maybe.option_map (\x -> x) (Prelude.snd i)))+ (Prelude.map (\i -> (,) (Prelude.id (Prelude.fst i))+ (Prelude.id (Prelude.snd i))) (ScanState.active maxReg sd))+ (Prelude.map (\i -> (,) (Prelude.id (Prelude.fst i))+ (Prelude.id (Prelude.snd i))) (ScanState.inactive maxReg sd))+ (Prelude.map (\i -> (,) (Prelude.id (Prelude.fst i))+ (Maybe.option_map (\x -> Prelude.id x) (Prelude.snd i))) (ScanState.handled maxReg sd)) data Details blockType1 blockType2 =
LinearScan/Monad.hs view
@@ -14,7 +14,7 @@ import qualified LinearScan.Applicative as Applicative import qualified LinearScan.Functor as Functor-import qualified LinearScan.List1 as List1+import qualified LinearScan.Seq as Seq __ :: any@@ -92,5 +92,5 @@ concatMapM :: (Applicative.Applicative a1) -> (a2 -> a1) -> ([] a2) -> a1 concatMapM h f l =- Functor.fmap (Applicative.is_functor h) List1.concat (mapM h f l)+ Functor.fmap (Applicative.is_functor h) Seq.flatten (mapM h f l)
LinearScan/Morph.hs view
@@ -139,7 +139,7 @@ in let { _evar_0_0 = \_ -> Prelude.Left ((:)- (Trace.ECannotSpillIfRegisterRequired ( i)) e)}+ (Trace.ECannotSpillIfRegisterRequired (Prelude.id i)) e)} in case Eqtype.eq_op (Eqtype.option_eqType@@ -178,7 +178,7 @@ in let { _evar_0_0 = \_ -> Prelude.Left ((:) (Trace.ERegisterAlreadyAssigned- ( reg)) e)}+ (Prelude.id reg)) e)} in case Prelude.not (Ssrbool.in_mem (unsafeCoerce reg)
LinearScan/Resolve.hs view
@@ -102,13 +102,13 @@ weakenResolvingMove :: Prelude.Int -> ResolvingMove -> ResolvingMoveSet weakenResolvingMove maxReg x = case x of {- 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 -> RSAllocReg fv ( tr);- FreeReg fr tv -> RSFreeReg ( fr) tv;- AssignReg fv tr -> RSAssignReg fv ( tr);- ClearReg fr tv -> RSClearReg ( fr) tv;+ Move fr fv tr -> RSMove (Prelude.id fr) fv (Prelude.id tr);+ Spill fr tv b -> RSSpill (Prelude.id fr) tv b;+ Restore fv tr b -> RSRestore fv (Prelude.id tr) b;+ AllocReg fv tr -> RSAllocReg fv (Prelude.id tr);+ FreeReg fr tv -> RSFreeReg (Prelude.id fr) tv;+ AssignReg fv tr -> RSAssignReg fv (Prelude.id tr);+ ClearReg fr tv -> RSClearReg (Prelude.id fr) tv; AllocStack tv -> RSAllocStack tv; FreeStack fv -> RSFreeStack fv; Looped x0 -> RSLooped (weakenResolvingMove maxReg x0)}
LinearScan/Seq.hs view
@@ -241,3 +241,7 @@ (iota ((Prelude.succ) m) n')) n +flatten :: ([] ([] a1)) -> [] a1+flatten =+ Prelude.foldr (Prelude.++) []+
LinearScan/Spill.hs view
@@ -60,12 +60,12 @@ SpillCondition -> Trace.SpillConditionT coq_SpillConditionToT maxReg sd uid i x = case x of {- NewToHandled -> Trace.NewToHandledT ( uid);- UnhandledToHandled -> Trace.UnhandledToHandledT ( uid);- ActiveToHandled xid reg -> Trace.ActiveToHandledT ( xid)- ( (unsafeCoerce reg));- InactiveToHandled xid reg -> Trace.InactiveToHandledT ( xid)- ( (unsafeCoerce reg))}+ NewToHandled -> Trace.NewToHandledT (Prelude.id uid);+ UnhandledToHandled -> Trace.UnhandledToHandledT (Prelude.id uid);+ ActiveToHandled xid reg -> Trace.ActiveToHandledT (Prelude.id xid)+ (Prelude.id (unsafeCoerce reg));+ InactiveToHandled xid reg -> Trace.InactiveToHandledT (Prelude.id xid)+ (Prelude.id (unsafeCoerce reg))} optimalSplitPosition :: Interval.IntervalDesc -> Prelude.Int -> Prelude.Int -> Prelude.Int@@ -257,7 +257,8 @@ maxReg sd) (ScanState.intervals maxReg sd) - ( i1_1))) ( uid)+ ( i1_1)))+ (Prelude.id uid) ( i1_0)) (ScanState.fixedIntervals maxReg sd) us'@@ -281,11 +282,12 @@ _evar_0_3 = \_ _ -> Prelude.Left ((:) (Trace.ECannotModifyHandledInterval- ( uid)) e3)}+ (Prelude.id uid)) e3)} in case Prelude.not (Ssrbool.in_mem- (unsafeCoerce ( uid))+ (unsafeCoerce+ (Prelude.id uid)) (Ssrbool.mem (Seq.seq_predType (Fintype.ordinal_eqType@@ -320,7 +322,7 @@ maxReg sd) (ScanState.intervals maxReg sd) ( i1_1)))- ( xid) ( i1_0))+ (Prelude.id xid) ( i1_0)) (ScanState.fixedIntervals maxReg sd) unh' (Prelude.map Prelude.id@@ -361,11 +363,12 @@ _evar_0_4 = \_ _ -> Prelude.Left ((:) (Trace.ECannotModifyHandledInterval- ( xid)) e3)}+ (Prelude.id xid)) e3)} in case Prelude.not (Ssrbool.in_mem- (unsafeCoerce ( xid))+ (unsafeCoerce+ (Prelude.id xid)) (Ssrbool.mem (Seq.seq_predType (Fintype.ordinal_eqType@@ -400,7 +403,7 @@ maxReg sd) (ScanState.intervals maxReg sd) ( i1_1)))- ( xid) ( i1_0))+ (Prelude.id xid) ( i1_0)) (ScanState.fixedIntervals maxReg sd) unh' (Prelude.map Prelude.id@@ -441,11 +444,12 @@ _evar_0_5 = \_ _ -> Prelude.Left ((:) (Trace.ECannotModifyHandledInterval- ( xid)) e3)}+ (Prelude.id xid)) e3)} in case Prelude.not (Ssrbool.in_mem- (unsafeCoerce ( xid))+ (unsafeCoerce+ (Prelude.id xid)) (Ssrbool.mem (Seq.seq_predType (Fintype.ordinal_eqType@@ -575,7 +579,7 @@ in let { _evar_0_1 = \_ -> Prelude.Left ((:)- (Trace.EIntervalBeginsBeforeUnhandled ( uid)) e)}+ (Trace.EIntervalBeginsBeforeUnhandled (Prelude.id uid)) e)} in case (Prelude.<=) beg (Interval.ibeg d) of { Prelude.True -> _evar_0_0 __;
LinearScan/Split.hs view
@@ -78,8 +78,8 @@ Prelude.Either ([] Trace.SSTrace) ScanState.ScanStateSig splitUnhandledInterval maxReg sd uid beg us pos e =- (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitUnhandledInterval ( uid)- (coq_SplitPositionToT pos)) e) (\e2 ->+ (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitUnhandledInterval+ (Prelude.id uid) (coq_SplitPositionToT pos)) e) (\e2 -> let { _evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 -> let {int = Vector0.vnth _nextInterval_ ints uid0} in@@ -175,8 +175,8 @@ in let { _evar_0_0 = \_ _ -> Prelude.Left ((:)- (Trace.ECannotModifyHandledInterval ( uid0))- e2)}+ (Trace.ECannotModifyHandledInterval+ (Prelude.id uid0)) e2)} in case Prelude.not (Ssrbool.in_mem (unsafeCoerce uid0)@@ -220,7 +220,7 @@ let {_evar_0_2 = \_ -> Prelude.Right _top_assumption_} in let { _evar_0_3 = \_ -> Prelude.Left ((:)- (Trace.ENoValidSplitPosition ( uid0)) e)}+ (Trace.ENoValidSplitPosition (Prelude.id uid0)) e)} in case (Prelude.<=) ((Prelude.succ) 0) (Data.List.length@@ -239,7 +239,7 @@ in let { _evar_0_1 = \_ -> Prelude.Left ((:) (Trace.ENoValidSplitPosition- ( uid0)) e)}+ (Prelude.id uid0)) e)} in case (Prelude.<=) beg (Interval.ibeg ( int)) of { Prelude.True -> _evar_0_0 __;@@ -267,8 +267,8 @@ _evar_0_0 = \_top_assumption_ -> let { _evar_0_0 = \uid beg us ->- (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitCurrentInterval - ( uid) (coq_SplitPositionToT pos)) e) (\e2 _ _ _ _ ->+ (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitCurrentInterval+ (Prelude.id uid) (coq_SplitPositionToT pos)) e) (\e2 _ _ _ _ -> let { _evar_0_0 = \_nextInterval_ intervals0 fints unhandled0 _active_ _inactive_ _handled_ uid0 us0 _top_assumption_0 -> let {_evar_0_0 = \err -> Prelude.Left err} in@@ -305,7 +305,7 @@ ([] Trace.SSTrace) ScanState.ScanStateSig splitActiveOrInactiveInterval maxReg sd uid beg us xid pos reg hin e = (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitActiveOrInactiveInterval- ( xid)+ (Prelude.id xid) (case hin of { Prelude.Left _ -> Prelude.True; Prelude.Right _ -> Prelude.False}) (coq_SplitPositionToT pos)) e)@@ -361,8 +361,8 @@ in let { _evar_0_0 = \_ _ -> Prelude.Left ((:)- (Trace.ECannotModifyHandledInterval ( xid0))- e2)}+ (Trace.ECannotModifyHandledInterval+ (Prelude.id xid0)) e2)} in case Prelude.not (Ssrbool.in_mem (unsafeCoerce xid0)@@ -420,7 +420,7 @@ in let { _evar_0_1 = \_ -> Prelude.Left ((:) (Trace.ENoValidSplitPosition- ( xid0)) e2)}+ (Prelude.id xid0)) e2)} in case (Prelude.<=) beg (Interval.ibeg ( int)) of { Prelude.True -> _evar_0_0 __;@@ -473,8 +473,8 @@ let { _evar_0_1 = \aid aids iHaids -> (Prelude.flip (Prelude.$)) ((:)- (Trace.ESplitAssignedIntervalForReg ( aid) ( reg)- (coq_SplitPositionToT pos)) e) (\e2 ->+ (Trace.ESplitAssignedIntervalForReg (Prelude.id aid)+ (Prelude.id reg) (coq_SplitPositionToT pos)) e) (\e2 -> let { _evar_0_1 = \_ -> let {@@ -524,11 +524,11 @@ (ScanState.nextInterval maxReg _top_assumption_3)) (Fintype.ordinal_eqType maxReg))- (unsafeCoerce ((,) ( aid) reg))+ (unsafeCoerce ((,) (Prelude.id aid) reg)) (unsafeCoerce (ScanState.active maxReg _top_assumption_3)))) ((:) ((,)- ( aid) reg)+ (Prelude.id aid) reg) (ScanState.inactive maxReg _top_assumption_3)) (ScanState.handled maxReg _top_assumption_3)} in@@ -547,7 +547,8 @@ in _evar_0_3 __} in- case Ssrbool.in_mem (unsafeCoerce ((,) ( aid) reg))+ case Ssrbool.in_mem+ (unsafeCoerce ((,) (Prelude.id aid) reg)) (Ssrbool.mem (Seq.seq_predType (Eqtype.prod_eqType@@ -568,7 +569,7 @@ in let { _evar_0_2 = \_ -> Prelude.Left ((:)- (Trace.ECannotSplitSingleton ( aid)) e2)}+ (Trace.ECannotSplitSingleton (Prelude.id aid)) e2)} in case (Prelude.<=) beg (splitPosition@@ -608,7 +609,7 @@ PhysReg -> Prelude.Int -> Morph.SState () () () splitActiveIntervalForReg maxReg pre reg pos =- Context.context (Trace.ESplitActiveIntervalForReg ( reg)+ Context.context (Trace.ESplitActiveIntervalForReg (Prelude.id reg) (coq_SplitPositionToT (BeforePos pos))) (splitAssignedIntervalForReg maxReg pre reg (BeforePos pos) Prelude.True) @@ -617,7 +618,8 @@ () () () splitAnyInactiveIntervalForReg maxReg pre reg pos e ss = (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitAnyInactiveIntervalForReg- ( reg) (coq_SplitPositionToT (EndOfLifetimeHole pos))) e) (\e2 ->+ (Prelude.id reg) (coq_SplitPositionToT (EndOfLifetimeHole pos))) e)+ (\e2 -> (Prelude.flip (Prelude.$)) (\s -> splitAssignedIntervalForReg maxReg s reg (EndOfLifetimeHole pos) Prelude.False) (\_top_assumption_ ->
LinearScan/Verify.hs view
@@ -297,8 +297,8 @@ (unsafeCoerce alloc) (unsafeCoerce reg)) of { Prelude.True -> errorT maxReg mDict pc (AllocationDoesNotMatch var- (reg)- (alloc) pos idx);+ (Maybe.option_map (Maybe.option_map Prelude.id) reg)+ (Maybe.option_map (Maybe.option_map Prelude.id) alloc) pos idx); Prelude.False -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()} reserveReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->@@ -326,11 +326,12 @@ (Prelude.not (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce v) (unsafeCoerce var)))- (errorT maxReg mDict pc (RegAlreadyReservedToVar ( reg) v var));+ (errorT maxReg mDict pc (RegAlreadyReservedToVar (Prelude.id reg)+ v var)); Prelude.Nothing -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))- (addMove maxReg mDict pc (Resolve.RSAllocReg var ( reg)))+ (addMove maxReg mDict pc (Resolve.RSAllocReg var (Prelude.id reg))) isReserved :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Verified a1 a2 (Prelude.Maybe Blocks.VarId)@@ -346,7 +347,7 @@ checkReservation maxReg mDict pc reg var = Monad.bind (State0.coq_StateT_Monad mDict) (\st -> let {- err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)+ err = errorT maxReg mDict pc (VarNotReservedForReg var (Prelude.id reg) (Lens.view (Lens.stepdownl' (\_ -> reservation)) (Vector0.vnth maxReg (rsAllocs maxReg st) reg)) ((Prelude.succ) 0))}@@ -377,12 +378,12 @@ (Lens.set (\_ -> reservation) Prelude.Nothing)) (rsStack maxReg st))) mDict; Prelude.Nothing ->- errorT maxReg mDict pc (VarNotReservedForReg var ( reg)+ errorT maxReg mDict pc (VarNotReservedForReg var (Prelude.id reg) (Lens.view (Lens.stepdownl' (\_ -> reservation)) (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))+ (addMove maxReg mDict pc (Resolve.RSFreeReg (Prelude.id reg) var)) clearReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier -> PhysReg -> Blocks.VarId -> Verified a1 a2 ()@@ -402,7 +403,8 @@ (rsStack maxReg st))) mDict; Prelude.Nothing -> let {- err = errorT maxReg mDict pc (VarNotResidentForReg var ( reg)+ err = errorT maxReg mDict pc (VarNotResidentForReg var+ (Prelude.id reg) (Lens.view (Lens.stepdownl' (\_ -> residency)) (Vector0.vnth maxReg (rsAllocs maxReg st) reg)) ((Prelude.succ) ((Prelude.succ) 0)))}@@ -416,7 +418,7 @@ Prelude.Nothing -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))- (addMove maxReg mDict pc (Resolve.RSClearReg ( reg) var))+ (addMove maxReg mDict pc (Resolve.RSClearReg (Prelude.id reg) var)) assignReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier -> PhysReg -> Blocks.VarId -> Verified a1 a2 ()@@ -447,7 +449,8 @@ (rsAllocs maxReg st)); Prelude.Nothing -> let {- err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)+ err = errorT maxReg mDict pc (VarNotReservedForReg var+ (Prelude.id reg) (Lens.view (Lens.stepdownl' (\_ -> reservation)) (Vector0.vnth maxReg (rsAllocs maxReg st) reg)) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0))))}@@ -461,7 +464,7 @@ Prelude.Nothing -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))- (addMove maxReg mDict pc (Resolve.RSAssignReg var ( reg)))+ (addMove maxReg mDict pc (Resolve.RSAssignReg var (Prelude.id reg))) isResident :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Verified a1 a2 (Prelude.Maybe Blocks.VarId)@@ -479,8 +482,8 @@ Monad.bind (State0.coq_StateT_Monad mDict) (\st -> Monad.bind (State0.coq_StateT_Monad mDict) (\res -> let {- err = errorT maxReg mDict pc (VarNotResidentForReg var ( reg) res- ((Prelude.succ) 0))}+ err = errorT maxReg mDict pc (VarNotResidentForReg var+ (Prelude.id reg) res ((Prelude.succ) 0))} in case useVerifier of { VerifyEnabledStrict ->@@ -649,7 +652,8 @@ case Lens.view (Lens.stepdownl' (\_ -> reservation)) (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of { Prelude.Just v ->- errorT maxReg mDict pc (PhysRegAlreadyReservedForVar ( reg) v);+ errorT maxReg mDict pc (PhysRegAlreadyReservedForVar+ (Prelude.id reg) v); Prelude.Nothing -> case Prelude.filter (\i -> Eqtype.eq_op@@ -663,7 +667,7 @@ errorT maxReg mDict pc (AllocationDoesNotMatch (Interval.ivar (Allocate.intVal maxReg x)) Prelude.Nothing (Prelude.Just- ((Allocate.intReg maxReg x)))+ (Maybe.option_map Prelude.id (Allocate.intReg maxReg x))) (Prelude.pred pc) 0)}}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)); Prelude.Right var ->@@ -708,7 +712,8 @@ case Lens.view (Lens.stepdownl' (\_ -> reservation)) (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of { Prelude.Just v ->- errorT maxReg mDict pc (PhysRegAlreadyReservedForVar ( reg) v);+ errorT maxReg mDict pc (PhysRegAlreadyReservedForVar+ (Prelude.id reg) v); Prelude.Nothing -> case Prelude.filter (\i -> Eqtype.eq_op@@ -722,7 +727,7 @@ errorT maxReg mDict pc (AllocationDoesNotMatch (Interval.ivar (Allocate.intVal maxReg x)) Prelude.Nothing (Prelude.Just- ((Allocate.intReg maxReg x)))+ (Maybe.option_map Prelude.id (Allocate.intReg maxReg x))) (Prelude.pred pc) 0)}}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)); Prelude.Right var ->
linearscan.cabal view
@@ -1,5 +1,5 @@ name: linearscan-version: 0.11+version: 0.11.1 synopsis: Linear scan register allocator, formally verified in Coq homepage: http://github.com/jwiegley/linearscan license: BSD3@@ -60,20 +60,19 @@ LinearScan.Build LinearScan.Choice LinearScan.Class- LinearScan.Context LinearScan.Const+ LinearScan.Context+ LinearScan.Contravariant LinearScan.Cursor LinearScan.Datatypes- -- LinearScan.Either- -- LinearScan.Either0 LinearScan.Eqtype LinearScan.Fintype LinearScan.Functor LinearScan.Graph LinearScan.Identity+ LinearScan.Interval LinearScan.IntMap LinearScan.IntSet- LinearScan.Interval LinearScan.Lens LinearScan.Lib LinearScan.List0