module LinearScan.Build where
import Debug.Trace (trace, traceShow)
import qualified Prelude
import qualified Data.IntMap
import qualified Data.IntSet
import qualified Data.List
import qualified Data.Ord
import qualified Data.Functor.Identity
import qualified LinearScan.Utils
import qualified LinearScan.Blocks as Blocks
import qualified LinearScan.Datatypes as Datatypes
import qualified LinearScan.IntMap as IntMap
import qualified LinearScan.Interval as Interval
import qualified LinearScan.Lib as Lib
import qualified LinearScan.LiveSets as LiveSets
import qualified LinearScan.Morph as Morph
import qualified LinearScan.NonEmpty0 as NonEmpty0
import qualified LinearScan.Range as Range
import qualified LinearScan.ScanState as ScanState
import qualified LinearScan.UsePos as UsePos
import qualified LinearScan.Eqtype as Eqtype
import qualified LinearScan.Fintype as Fintype
import qualified LinearScan.Seq as Seq
import qualified LinearScan.Ssrbool as Ssrbool
import qualified LinearScan.Ssrfun as Ssrfun
import qualified LinearScan.Ssrnat as Ssrnat
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base as GHC.Base
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
import qualified LinearScan.IOExts as IOExts
unsafeCoerce = IOExts.unsafeCoerce
#endif
__ :: any
__ = Prelude.error "Logical or arity value used"
type BuildState = Data.IntMap.IntMap Range.SortedRanges
newBuildState :: Prelude.Int -> BuildState
newBuildState n =
IntMap.emptyIntMap
data RangeCursor =
Build_RangeCursor Prelude.Int Range.BoundedRange Range.SortedRanges
emptyRangeCursor :: Prelude.Int -> Prelude.Int -> Prelude.Int -> RangeCursor
emptyRangeCursor b pos e =
(Prelude.flip (Prelude.$)) __ (\_ -> Build_RangeCursor pos
(Range.emptyBoundedRange ((Prelude.succ) (Ssrnat.double b))
((Prelude.succ) (Ssrnat.double pos)))
(Range.emptySortedRanges ((Prelude.succ) (Ssrnat.double pos))))
transportRangeCursor :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
Prelude.Int -> RangeCursor -> RangeCursor
transportRangeCursor b prev base e c =
let {_evar_0_ = \mid r rs -> Build_RangeCursor mid r rs} in
case c of {
Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1}
type PendingRanges = (Data.IntMap.IntMap RangeCursor)
emptyPendingRanges :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
Prelude.Int -> Data.IntSet.IntSet -> PendingRanges
emptyPendingRanges maxReg b pos e liveOuts =
(Prelude.flip (Prelude.$)) (emptyRangeCursor b pos e) (\empty ->
(Prelude.flip (Prelude.$)) (\xs vid ->
Data.IntMap.insert ((Prelude.+) vid maxReg) empty xs) (\f ->
Data.IntSet.foldl' f IntMap.emptyIntMap liveOuts))
mergeIntoSortedRanges :: Prelude.Int -> Prelude.Int -> PendingRanges ->
(Data.IntMap.IntMap Range.SortedRanges) ->
Data.IntMap.IntMap Range.SortedRanges
mergeIntoSortedRanges b pos pmap rmap =
Data.IntMap.mergeWithKey (\_the_1st_wildcard_ _top_assumption_ ->
let {
_evar_0_ = \mid br ps rs ->
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
ps' = Range.prependRange ((Prelude.succ) (Ssrnat.double b))
((Prelude.succ) (Ssrnat.double mid)) br ps ((Prelude.succ)
(Ssrnat.double b))}
in
Prelude.Just
(Range.coq_SortedRanges_cat ((Prelude.succ) (Ssrnat.double b)) ps'
((Prelude.succ) (Ssrnat.double pos)) rs))}
in
(\rs ->
case _top_assumption_ of {
Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1 rs}))
(Data.IntMap.map (\_top_assumption_ ->
let {
_evar_0_ = \_cursorMid_ br rs ->
(Prelude.flip (Prelude.$)) __ (\_ ->
(Range.prependRange ((Prelude.succ) (Ssrnat.double b))
((Prelude.succ) (Ssrnat.double _cursorMid_)) br rs
((Prelude.succ) (Ssrnat.double b))))}
in
case _top_assumption_ of {
Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1}))
(Data.IntMap.map
(Range.transportSortedRanges ((Prelude.succ) (Ssrnat.double b))
((Prelude.succ) (Ssrnat.double pos)))) ( pmap) rmap
varKindLtn :: Blocks.VarKind -> Blocks.VarKind -> Prelude.Bool
varKindLtn x y =
case x of {
Blocks.Input ->
case y of {
Blocks.Input -> Prelude.False;
_ -> Prelude.True};
Blocks.Temp ->
case y of {
Blocks.Output -> Prelude.True;
_ -> Prelude.False};
Blocks.Output -> Prelude.False}
handleVars_combine :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
Prelude.Int -> RangeCursor -> ((,) Prelude.Bool
([] Blocks.VarKind)) -> Prelude.Maybe RangeCursor
handleVars_combine b pos e vid range vars =
let {
_evar_0_ = \mid br srs ->
let {
_evar_0_ = \req kinds ->
let {
upos = UsePos.Build_UsePos ((Prelude.succ) (Ssrnat.double pos)) req}
in
(Prelude.flip (Prelude.$)) __ (\_ ->
(Prelude.flip (Prelude.$)) __ (\_ ->
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
_evar_0_ = \_ ->
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
r2 = Range.coq_Range_cons upos (Range.Build_RangeDesc
((Prelude.succ) (Ssrnat.double pos))
(Range.rend ( br)) (Range.ups ( br)))}
in
Prelude.Just (Build_RangeCursor mid r2 srs))}
in
let {
_evar_0_0 = \_ ->
let {
_evar_0_0 = \_ ->
(Prelude.flip (Prelude.$)) __ (\_ ->
let {r1 = Range.coq_Range_cons upos ( ( br))} in
Prelude.Just (Build_RangeCursor mid r1 srs))}
in
let {
_evar_0_1 = \_ ->
let {r1 = Range.newRange upos} in
let {
_evar_0_1 = \_ ->
(Prelude.flip (Prelude.$)) __ (\_ -> Prelude.Just
(Build_RangeCursor ((Prelude.succ) pos) r1
(
(Range.prependRange ((Prelude.succ) (Ssrnat.double b))
((Prelude.succ) (Ssrnat.double mid)) br srs
((Prelude.succ)
(Ssrnat.double ((Prelude.succ) pos)))))))}
in
_evar_0_1 __}
in
case (Prelude.<=) (Range.rbeg ( ( br))) (UsePos.uloc upos) of {
Prelude.True -> _evar_0_0 __;
Prelude.False -> _evar_0_1 __}}
in
case (Prelude.&&)
(Ssrbool.in_mem (unsafeCoerce Blocks.Output)
(Ssrbool.mem
(Seq.seq_predType Blocks.coq_VarKind_eqType) kinds))
(Prelude.not
(Ssrbool.in_mem (unsafeCoerce Blocks.Input)
(Ssrbool.mem
(Seq.seq_predType Blocks.coq_VarKind_eqType) kinds))) of {
Prelude.True -> _evar_0_ __;
Prelude.False -> _evar_0_0 __})))}
in
case vars of {
(,) x x0 -> unsafeCoerce _evar_0_ x x0}}
in
case range of {
Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1}
handleVars_onlyRanges :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
(Data.IntMap.IntMap RangeCursor) ->
Data.IntMap.IntMap RangeCursor
handleVars_onlyRanges b pos e =
Data.IntMap.map (transportRangeCursor b ((Prelude.succ) pos) pos e)
handleVars_onlyVars :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
(Data.IntMap.IntMap
((,) Prelude.Bool ([] Blocks.VarKind))) ->
Data.IntMap.IntMap RangeCursor
handleVars_onlyVars b pos e =
Data.IntMap.map (\_top_assumption_ ->
let {
_evar_0_ = \req kinds ->
let {
rd = Range.Build_RangeDesc
(case Ssrbool.in_mem (unsafeCoerce Blocks.Input)
(Ssrbool.mem (Seq.seq_predType Blocks.coq_VarKind_eqType)
kinds) of {
Prelude.True -> (Prelude.succ) (Ssrnat.double b);
Prelude.False -> (Prelude.succ) (Ssrnat.double pos)})
(case Ssrbool.in_mem (unsafeCoerce Blocks.Output)
(Ssrbool.mem (Seq.seq_predType Blocks.coq_VarKind_eqType)
kinds) of {
Prelude.True -> (Prelude.succ) (Ssrnat.double e);
Prelude.False -> (Prelude.succ) ((Prelude.succ)
(Ssrnat.double pos))}) ((:) (UsePos.Build_UsePos ((Prelude.succ)
(Ssrnat.double pos)) req) [])}
in
Build_RangeCursor e rd []}
in
case _top_assumption_ of {
(,) x x0 -> unsafeCoerce _evar_0_ x x0})
extractVarInfo :: Prelude.Int -> ([] Blocks.VarInfo) -> (,) Prelude.Bool
([] Blocks.VarKind)
extractVarInfo maxReg xs =
(,)
(Prelude.not
(Eqtype.eq_op Ssrnat.nat_eqType
(unsafeCoerce (Seq.find (Blocks.regRequired maxReg) xs))
(unsafeCoerce (Data.List.length xs))))
(Lib.sortBy varKindLtn (Prelude.map (\v -> Blocks.varKind maxReg v) xs))
handleVars :: Prelude.Int -> ([] Blocks.VarInfo) -> Prelude.Int ->
Prelude.Int -> Prelude.Int -> PendingRanges -> PendingRanges
handleVars maxReg varRefs b pos e ranges =
let {
vars = Data.IntMap.map (extractVarInfo maxReg)
(IntMap.coq_IntMap_groupOn (Blocks.nat_of_varId maxReg) varRefs)}
in
Data.IntMap.mergeWithKey (handleVars_combine b pos e)
(handleVars_onlyRanges b pos e) (handleVars_onlyVars b pos e) ( ranges)
vars
reduceOp :: Prelude.Int -> (Blocks.OpInfo a4 a2 a3) -> Prelude.Int ->
Prelude.Int -> Prelude.Int -> a1 -> a2 -> PendingRanges ->
PendingRanges
reduceOp maxReg oinfo b pos e block op ranges =
let {refs = Blocks.opRefs maxReg oinfo op} in
let {
refs' = case Blocks.opKind maxReg oinfo op of {
Blocks.IsCall ->
(Prelude.++)
(Fintype.image_mem (Fintype.ordinal_finType maxReg) (\n ->
Blocks.Build_VarInfo (Prelude.Left (unsafeCoerce n))
Blocks.Temp Prelude.True)
(Ssrbool.mem
(Seq.seq_predType (Fintype.ordinal_eqType maxReg))
(unsafeCoerce (Fintype.ord_enum maxReg)))) refs;
_ -> refs}}
in
handleVars maxReg refs' b pos e ranges
reduceBlock :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->
(Blocks.OpInfo a5 a3 a4) -> Prelude.Int -> a1 -> PendingRanges
-> PendingRanges
reduceBlock maxReg binfo oinfo pos block =
let {sz = Blocks.blockSize binfo block} in
let {e = (Prelude.+) pos sz} in
let {ops = Blocks.allBlockOps binfo block} in
let {
_evar_0_ = let {_evar_0_ = let {_evar_0_ = \h -> h} in _evar_0_} in
let {
_evar_0_0 = \o os iHos ->
let {
_evar_0_0 = \ranges ->
iHos
(reduceOp maxReg oinfo pos
((Prelude.+) pos (Data.List.length os)) e block o
ranges)}
in
_evar_0_0}
in
Datatypes.list_rec _evar_0_ _evar_0_0 (Seq.rev ops)}
in
_evar_0_
reduceBlocks :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->
(Blocks.OpInfo a5 a3 a4) -> ([] a1) -> (Data.IntMap.IntMap
LiveSets.BlockLiveSets) -> Prelude.Int -> BuildState
reduceBlocks maxReg binfo oinfo blocks liveSets pos =
let {_evar_0_ = \pos0 -> newBuildState pos0} in
let {
_evar_0_0 = \b blocks0 iHbs pos0 ->
(Prelude.flip (Prelude.$)) (Blocks.blockId binfo b) (\bid ->
(Prelude.flip (Prelude.$))
(case Data.IntMap.lookup bid liveSets of {
Prelude.Just ls -> LiveSets.blockLiveOut ls;
Prelude.Nothing -> Data.IntSet.empty}) (\outs ->
let {sz = Blocks.blockSize binfo b} in
let {
_evar_0_0 = \_ ->
let {endpos = (Prelude.+) pos0 sz} in
(Prelude.flip (Prelude.$)) __ (\_ ->
(Prelude.flip (Prelude.$)) __ (\_ ->
(Prelude.flip (Prelude.$))
(reduceBlock maxReg binfo oinfo pos0 b
(emptyPendingRanges maxReg pos0 endpos endpos outs))
(\pending ->
mergeIntoSortedRanges pos0 endpos pending (iHbs endpos))))}
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_rec _evar_0_ _evar_0_0 blocks pos
compileIntervals :: Prelude.Int -> Prelude.Int -> BuildState -> (,)
ScanState.FixedIntervalsType
(Data.IntMap.IntMap Interval.IntervalDesc)
compileIntervals maxReg pos bs =
Data.IntMap.foldlWithKey (\_top_assumption_ ->
let {
_evar_0_ = \regs vars vid rs ->
let {_evar_0_ = \_ -> (,) regs vars} in
let {
_evar_0_0 = \_a_ _l_ ->
let {
_evar_0_0 = \_ -> (,)
(LinearScan.Utils.set_nth maxReg regs ( vid) (Prelude.Just
(Interval.packInterval (Interval.Build_IntervalDesc vid
(Range.rbeg
( (Prelude.head (NonEmpty0.coq_NE_from_list _a_ _l_))))
(Range.rend
( (Prelude.last (NonEmpty0.coq_NE_from_list _a_ _l_))))
Interval.Whole (NonEmpty0.coq_NE_from_list _a_ _l_))))) vars}
in
let {
_evar_0_1 = \_ ->
(Prelude.flip (Prelude.$)) ((Prelude.-) vid maxReg) (\vid' -> (,)
regs
(Data.IntMap.insert vid'
(Interval.packInterval (Interval.Build_IntervalDesc vid'
(Range.rbeg
( (Prelude.head (NonEmpty0.coq_NE_from_list _a_ _l_))))
(Range.rend
( (Prelude.last (NonEmpty0.coq_NE_from_list _a_ _l_))))
Interval.Whole (NonEmpty0.coq_NE_from_list _a_ _l_))) vars))}
in
case (Prelude.<=) ((Prelude.succ) vid) maxReg of {
Prelude.True -> _evar_0_0 __;
Prelude.False -> _evar_0_1 __}}
in
case (Ssrfun.sig_of_sig2 rs) of {
[] -> _evar_0_ __;
(:) x x0 -> _evar_0_0 x x0}}
in
case _top_assumption_ of {
(,) x x0 -> _evar_0_ x x0}) ((,)
(Data.List.replicate maxReg Prelude.Nothing) IntMap.emptyIntMap) bs
buildIntervals :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->
(Blocks.OpInfo a5 a3 a4) -> ([] a1) -> (Data.IntMap.IntMap
LiveSets.BlockLiveSets) -> Prelude.Either Morph.SSError
ScanState.ScanStateSig
buildIntervals maxReg binfo oinfo blocks liveSets =
let {
handleVar = \ss i ->
ScanState.packScanState maxReg ScanState.Pending
(ScanState.Build_ScanStateDesc ((Prelude.succ)
(ScanState.nextInterval maxReg ( ss)))
(LinearScan.Utils.snoc (ScanState.nextInterval maxReg ( ss))
(ScanState.intervals maxReg ( ss)) ( i))
(ScanState.fixedIntervals maxReg ( ss))
(Lib.insert (Lib.lebf Prelude.snd) ((,)
( (ScanState.nextInterval maxReg ( ss))) (Interval.ibeg ( i)))
(Prelude.map Prelude.id (ScanState.unhandled maxReg ( ss))))
(Prelude.map Prelude.id (ScanState.active maxReg ( ss)))
(Prelude.map Prelude.id (ScanState.inactive maxReg ( ss)))
(Prelude.map Prelude.id (ScanState.handled maxReg ( ss))))}
in
case blocks of {
[] -> Prelude.Right
(ScanState.packScanState maxReg ScanState.InUse
(ScanState.Build_ScanStateDesc 0 []
(Data.List.replicate maxReg Prelude.Nothing) [] [] [] []));
(:) b bs ->
let {bs0 = reduceBlocks maxReg binfo oinfo ((:) b bs) liveSets 0} in
case compileIntervals maxReg 0 bs0 of {
(,) regs vars ->
let {
s2 = ScanState.packScanState maxReg ScanState.Pending
(ScanState.Build_ScanStateDesc
(ScanState.nextInterval maxReg (ScanState.Build_ScanStateDesc 0
[] (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))
(ScanState.intervals maxReg (ScanState.Build_ScanStateDesc 0 []
(Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))
regs
(ScanState.unhandled maxReg (ScanState.Build_ScanStateDesc 0 []
(Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))
(ScanState.active maxReg (ScanState.Build_ScanStateDesc 0 []
(Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))
(ScanState.inactive maxReg (ScanState.Build_ScanStateDesc 0 []
(Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))
(ScanState.handled maxReg (ScanState.Build_ScanStateDesc 0 []
(Data.List.replicate maxReg Prelude.Nothing) [] [] [] [])))}
in
let {s3 = Data.IntMap.foldl handleVar s2 vars} in
Prelude.Right (ScanState.packScanState maxReg ScanState.InUse ( s3))}}