module LinearScan.Interval 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.Lib as Lib import qualified LinearScan.Logic as Logic import qualified LinearScan.Range as Range import qualified LinearScan.UsePos as UsePos __ :: any __ = Prelude.error "Logical or arity value used" data IntervalKind = Whole | LeftMost | Middle | RightMost splitKind :: IntervalKind -> (,) IntervalKind IntervalKind splitKind k = case k of { Whole -> (,) LeftMost RightMost; LeftMost -> (,) LeftMost Middle; Middle -> (,) Middle Middle; RightMost -> (,) Middle RightMost} data IntervalDesc = Build_IntervalDesc Prelude.Int Prelude.Int Prelude.Int IntervalKind ([] Range.RangeDesc) ivar :: IntervalDesc -> Prelude.Int ivar i = case i of { Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> ivar0} ibeg :: IntervalDesc -> Prelude.Int ibeg i = case i of { Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> ibeg0} iend :: IntervalDesc -> Prelude.Int iend i = case i of { Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> iend0} iknd :: IntervalDesc -> IntervalKind iknd i = case i of { Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> iknd0} rds :: IntervalDesc -> [] Range.RangeDesc rds i = case i of { Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> rds0} getIntervalDesc :: IntervalDesc -> IntervalDesc getIntervalDesc d = d packInterval :: IntervalDesc -> IntervalDesc packInterval d = d intervalStart :: IntervalDesc -> Prelude.Int intervalStart i = ibeg i intervalEnd :: IntervalDesc -> Prelude.Int intervalEnd i = iend i intervalCoversPos :: IntervalDesc -> Prelude.Int -> Prelude.Bool intervalCoversPos d pos = (Prelude.&&) ((Prelude.<=) (intervalStart d) pos) ((Prelude.<=) ((Prelude.succ) pos) (intervalEnd d)) intervalsIntersect :: IntervalDesc -> IntervalDesc -> Prelude.Bool intervalsIntersect i j = let {f = \x y -> Range.rangesIntersect ( x) ( y)} in Data.List.any (\x -> Data.List.any (f x) ( (rds j))) ( (rds i)) intervalIntersectionPoint :: IntervalDesc -> IntervalDesc -> Prelude.Maybe Lib.Coq_oddnum intervalIntersectionPoint i j = Data.List.foldl' (\acc rd -> case acc of { Prelude.Just x -> Prelude.Just x; Prelude.Nothing -> Data.List.foldl' (\acc' rd' -> case acc' of { Prelude.Just x -> Prelude.Just x; Prelude.Nothing -> Range.rangeIntersectionPoint ( rd) ( rd')}) Prelude.Nothing (rds j)}) Prelude.Nothing (rds i) searchInRange :: Range.RangeDesc -> (UsePos.UsePos -> Prelude.Bool) -> Prelude.Maybe ((,) Range.RangeDesc UsePos.UsePos) searchInRange r f = let {_evar_0_ = \x -> Prelude.Just ((,) r x)} in let {_evar_0_0 = Prelude.Nothing} in case Range.findRangeUsePos ( r) f of { Prelude.Just x -> _evar_0_ x; Prelude.Nothing -> _evar_0_0} findIntervalUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) -> Prelude.Maybe ((,) Range.RangeDesc UsePos.UsePos) findIntervalUsePos d f = let { go rs = (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs) (\r -> searchInRange r f) (\r rs' -> Lib.option_choose (searchInRange r f) (go rs')) rs} in go (rds d) lookupUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) -> Prelude.Maybe Lib.Coq_oddnum lookupUsePos d f = let { _evar_0_ = \_top_assumption_ -> let { _evar_0_ = \r _top_assumption_0 -> Prelude.Just (UsePos.uloc _top_assumption_0)} in case _top_assumption_ of { (,) x x0 -> _evar_0_ x x0}} in let {_evar_0_0 = Prelude.Nothing} in case findIntervalUsePos d f of { Prelude.Just x -> _evar_0_ x; Prelude.Nothing -> _evar_0_0} nextUseAfter :: IntervalDesc -> Prelude.Int -> Prelude.Maybe Lib.Coq_oddnum nextUseAfter d pos = lookupUsePos d (\u -> (Prelude.<=) ((Prelude.succ) pos) (UsePos.uloc u)) firstUsePos :: IntervalDesc -> Prelude.Maybe Prelude.Int firstUsePos d = case Range.ups ( (Prelude.head (rds d))) of { [] -> Prelude.Nothing; (:) u l -> Prelude.Just (UsePos.uloc u)} firstUseReqReg :: IntervalDesc -> Prelude.Maybe Lib.Coq_oddnum firstUseReqReg d = lookupUsePos d UsePos.regReq intervalSpan :: ([] Range.RangeDesc) -> Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int -> IntervalKind -> ((,) (Prelude.Maybe IntervalDesc) (Prelude.Maybe IntervalDesc)) intervalSpan rs before iv ib ie knd = let { _evar_0_ = \lknd rknd -> (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs) (\r -> let {_top_assumption_ = Range.rangeSpan before ( r)} in let { _evar_0_ = \_top_assumption_0 -> let { _evar_0_ = \r0 _top_assumption_1 -> let { _evar_0_ = \r1 -> let { _evar_0_ = let { _evar_0_ = \_ _ -> (,) (Prelude.Just (packInterval (Build_IntervalDesc iv (Range.rbeg ( r0)) (Range.rend ( r0)) lknd ((:[]) ( r0))))) (Prelude.Just (packInterval (Build_IntervalDesc iv (Range.rbeg ( r1)) (Range.rend ( r1)) rknd ((:[]) ( r1)))))} in _evar_0_} in _evar_0_ __ __} in let { _evar_0_0 = let { _evar_0_0 = let { _evar_0_0 = \_ -> (,) (Prelude.Just (packInterval (Build_IntervalDesc iv (Range.rbeg ( r0)) (Range.rend ( r0)) knd ((:[]) ( r0))))) Prelude.Nothing} in _evar_0_0} in _evar_0_0} in case _top_assumption_1 of { Prelude.Just x -> (\_ -> _evar_0_ x); Prelude.Nothing -> _evar_0_0}} in let { _evar_0_0 = \_top_assumption_1 -> let { _evar_0_0 = \r1 -> let { _evar_0_0 = let { _evar_0_0 = \_ -> (,) Prelude.Nothing (Prelude.Just (packInterval (Build_IntervalDesc iv (Range.rbeg ( r1)) (Range.rend ( r1)) knd ((:[]) ( r1)))))} in _evar_0_0} in _evar_0_0} in let {_evar_0_1 = \_ -> Logic.coq_False_rec} in case _top_assumption_1 of { Prelude.Just x -> _evar_0_0 x; Prelude.Nothing -> _evar_0_1}} in case _top_assumption_0 of { Prelude.Just x -> _evar_0_ x; Prelude.Nothing -> _evar_0_0}} in case _top_assumption_ of { (,) x x0 -> _evar_0_ x x0 __}) (\r rs0 -> let {_top_assumption_ = Range.rangeSpan before ( r)} in let { _evar_0_ = \_top_assumption_0 -> let { _evar_0_ = \r0 _top_assumption_1 -> let { _evar_0_ = \r1 -> let { _evar_0_ = \_ -> (Prelude.flip (Prelude.$)) __ (\_ -> let { _evar_0_ = \_ -> (,) (Prelude.Just (packInterval (Build_IntervalDesc iv (Range.rbeg ( r0)) (Range.rend ( r0)) lknd ((:[]) ( r0))))) (Prelude.Just (packInterval (Build_IntervalDesc iv (Range.rbeg ( r1)) (Range.rend ( (Prelude.last rs0))) rknd ((:) r1 rs0))))} in _evar_0_ __)} in _evar_0_ __} in let { _evar_0_0 = \_ -> let { _evar_0_0 = \_ -> let { _top_assumption_2 = intervalSpan rs0 before iv (Range.rbeg ( (Prelude.head rs0))) (Range.rend ( (Prelude.last rs0))) knd} in let { _evar_0_0 = \_top_assumption_3 -> let { _evar_0_0 = \i1_1 _top_assumption_4 -> let { _evar_0_0 = \i1_2 -> case i1_1 of { Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> let { _evar_0_0 = let { _evar_0_0 = \_ -> let { _evar_0_0 = \_ -> let { _evar_0_0 = \_ -> (Prelude.flip (Prelude.$)) __ (\_ -> let { _evar_0_0 = let { _evar_0_0 = \_ _ _ -> (,) (Prelude.Just (packInterval (Build_IntervalDesc ivar0 (Range.rbeg ( r)) iend0 lknd ((:) r rds0)))) (Prelude.Just (packInterval (Build_IntervalDesc (ivar ( i1_2)) (ibeg ( i1_2)) (iend ( i1_2)) rknd (rds ( i1_2)))))} in _evar_0_0 __} in _evar_0_0)} in _evar_0_0 __} in _evar_0_0 __} in _evar_0_0} in _evar_0_0 __}} in let { _evar_0_1 = \_ _ _ -> case i1_1 of { Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> let { _evar_0_1 = let { _evar_0_1 = \_ -> (Prelude.flip (Prelude.$)) __ (\_ -> (Prelude.flip (Prelude.$)) __ (\_ -> let { _evar_0_1 = \_ -> let { _evar_0_1 = \_ -> (,) (Prelude.Just (packInterval (Build_IntervalDesc ivar0 (Range.rbeg ( r)) iend0 lknd ((:) r rds0)))) Prelude.Nothing} in _evar_0_1 __} in _evar_0_1 __))} in _evar_0_1} in _evar_0_1 __}} in case _top_assumption_4 of { Prelude.Just x -> (\_ -> _evar_0_0 x); Prelude.Nothing -> _evar_0_1}} in let { _evar_0_1 = \_top_assumption_4 -> let { _evar_0_1 = \i1_2 -> case i1_2 of { Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> let { _evar_0_1 = let { _evar_0_1 = \_ -> let { _evar_0_1 = \_ _ -> let { _evar_0_1 = \_ -> let { _evar_0_1 = \_ -> let { _evar_0_1 = \_ -> (Prelude.flip (Prelude.$)) __ (\_ -> (,) (Prelude.Just (packInterval (Build_IntervalDesc iv (Range.rbeg ( r0)) (Range.rend ( r0)) lknd ((:[]) ( r0))))) (Prelude.Just (packInterval (Build_IntervalDesc (ivar (Build_IntervalDesc ivar0 (Range.rbeg ( (Prelude.head rds0))) (Range.rend ( (Prelude.last rds0))) iknd0 rds0)) (ibeg (Build_IntervalDesc ivar0 (Range.rbeg ( (Prelude.head rds0))) (Range.rend ( (Prelude.last rds0))) iknd0 rds0)) (iend (Build_IntervalDesc ivar0 (Range.rbeg ( (Prelude.head rds0))) (Range.rend ( (Prelude.last rds0))) iknd0 rds0)) rknd (rds (Build_IntervalDesc ivar0 (Range.rbeg ( (Prelude.head rds0))) (Range.rend ( (Prelude.last rds0))) iknd0 rds0))))))} in _evar_0_1 __} in _evar_0_1 __} in _evar_0_1 __} in _evar_0_1 __ __} in _evar_0_1} in _evar_0_1 __}} in let {_evar_0_2 = \_ _ _ -> Logic.coq_False_rec} in case _top_assumption_4 of { Prelude.Just x -> (\_ _ _ -> _evar_0_1 x); Prelude.Nothing -> _evar_0_2}} in case _top_assumption_3 of { Prelude.Just x -> _evar_0_0 x; Prelude.Nothing -> _evar_0_1}} in case _top_assumption_2 of { (,) x x0 -> _evar_0_0 x x0 __ __ __}} in _evar_0_0 __} in case _top_assumption_1 of { Prelude.Just x -> (\_ -> _evar_0_ x); Prelude.Nothing -> _evar_0_0}} in let { _evar_0_0 = \_top_assumption_1 -> let { _evar_0_0 = \r1 -> let { _evar_0_0 = \_ -> let { _evar_0_0 = \_ -> let { _evar_0_0 = \_ -> (,) Prelude.Nothing (Prelude.Just (packInterval (Build_IntervalDesc iv (Range.rbeg ( r1)) (Range.rend ( (Prelude.last rs0))) knd ((:) r1 rs0))))} in _evar_0_0 __} in _evar_0_0 __} in _evar_0_0 __} in let {_evar_0_1 = \_ -> Logic.coq_False_rec} in case _top_assumption_1 of { Prelude.Just x -> (\_ -> _evar_0_0 x); Prelude.Nothing -> _evar_0_1}} in case _top_assumption_0 of { Prelude.Just x -> _evar_0_ x; Prelude.Nothing -> _evar_0_0}} in case _top_assumption_ of { (,) x x0 -> _evar_0_ x x0 __}) rs} in case splitKind knd of { (,) x x0 -> _evar_0_ x x0}