{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}

module LinearScan.Interval 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

import qualified LinearScan.List1 as List1
import qualified LinearScan.Logic as Logic
import qualified LinearScan.Maybe as Maybe
import qualified LinearScan.NonEmpty as NonEmpty
import qualified LinearScan.Prelude0 as Prelude0
import qualified LinearScan.Range as Range
import qualified LinearScan.Specif as Specif
import qualified LinearScan.UsePos as UsePos
import qualified LinearScan.Eqtype as Eqtype
import qualified LinearScan.Seq as Seq
import qualified LinearScan.Ssrnat as Ssrnat



#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__
--unsafeCoerce :: a -> b
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
--unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif

__ :: any
__ = Prelude.error "Logical or arity value used"

data IntervalDesc =
   Build_IntervalDesc Prelude.Int Prelude.Int Prelude.Int ([]
                                                          Range.RangeDesc)

ivar :: IntervalDesc -> Prelude.Int
ivar i =
  case i of {
   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> ivar0}

ibeg :: IntervalDesc -> Prelude.Int
ibeg i =
  case i of {
   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> ibeg0}

iend :: IntervalDesc -> Prelude.Int
iend i =
  case i of {
   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> iend0}

rds :: IntervalDesc -> [] Range.RangeDesc
rds i =
  case i of {
   Build_IntervalDesc ivar0 ibeg0 iend0 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

posWithinInterval :: IntervalDesc -> Prelude.Int -> Prelude.Bool
posWithinInterval d pos =
  (Prelude.&&) ((Prelude.<=) (intervalStart d) pos)
    ((Prelude.<=) ((Prelude.succ) pos) (intervalEnd d))

intervalsOverlap :: IntervalDesc -> IntervalDesc -> Prelude.Maybe Prelude.Int
intervalsOverlap i j =
  Data.List.foldl' (\acc xr ->
    Data.List.foldl' (\acc' yr ->
      Maybe.option_choose acc'
        (Range.rangesIntersect (Range.getRangeDesc ( xr))
          (Range.getRangeDesc ( yr)))) acc (rds j)) Prelude.Nothing (rds i)

findIntervalUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) ->
                      Prelude.Maybe
                      ((,) Range.RangeDesc (Specif.Coq_sig2 UsePos.UsePos))
findIntervalUsePos d f =
  let {
   _evar_0_ = \_ ->
    let {
     _evar_0_ = \_ ->
      let {
       _evar_0_ = \r ->
        let {_top_assumption_ = Range.findRangeUsePos ( r) f} in
        let {
         _evar_0_ = \_top_assumption_0 -> Prelude.Just ((,) r
          _top_assumption_0)}
        in
        let {_evar_0_0 = Prelude.Nothing} in
        case _top_assumption_ of {
         Prelude.Just x -> _evar_0_ x;
         Prelude.Nothing -> _evar_0_0}}
      in
      let {
       _evar_0_0 = \r rs iHrs ->
        let {_top_assumption_ = Range.findRangeUsePos ( r) f} in
        let {
         _evar_0_0 = \_top_assumption_0 -> Prelude.Just ((,) r
          _top_assumption_0)}
        in
        let {_evar_0_1 = iHrs __ __ __} in
        case _top_assumption_ of {
         Prelude.Just x -> _evar_0_0 x;
         Prelude.Nothing -> _evar_0_1}}
      in
      NonEmpty.coq_NonEmpty_rec (\r _ _ _ -> _evar_0_ r) (\r rs iHrs _ _ _ ->
        _evar_0_0 r rs iHrs) (rds d) __ __ __}
    in
     _evar_0_ __}
  in
   _evar_0_ __

lookupUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) ->
                Prelude.Maybe Prelude0.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}

intervalHasInputsAt :: IntervalDesc -> Prelude.Int -> Prelude.Bool
intervalHasInputsAt d pos =
  Data.List.foldl' (\b r -> (Prelude.||) b (Range.hasInputsAt ( r) pos))
    Prelude.False (rds d)

nextUseAfter :: IntervalDesc -> Prelude.Int -> Prelude.Maybe
                Prelude0.Coq_oddnum
nextUseAfter d pos =
  case lookupUsePos d (\u ->
         (Prelude.<=) ((Prelude.succ) pos) (UsePos.uloc u)) of {
   Prelude.Just s -> Prelude.Just s;
   Prelude.Nothing -> Prelude.Nothing}

rangeFirstUsePos :: Range.RangeDesc -> Prelude.Maybe UsePos.UsePos
rangeFirstUsePos rd =
  case Range.ups rd of {
   [] -> Prelude.Nothing;
   (:) u l -> Prelude.Just u}

posAtRangeEnd :: IntervalDesc -> Prelude.Int -> Prelude.Bool
posAtRangeEnd d pos =
  let {
   go xs =
     (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
       (\x ->
       Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Range.rend ( x)))
         (unsafeCoerce pos))
       (\x xs0 ->
       (Prelude.||)
         (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Range.rend ( x)))
           (unsafeCoerce pos)) (go xs0))
       xs}
  in go (rds d)

firstUsePos :: IntervalDesc -> Prelude.Maybe UsePos.UsePos
firstUsePos d =
  let {
   go xs =
     (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
       (\x ->
       rangeFirstUsePos ( x))
       (\x xs0 ->
       Maybe.option_choose (rangeFirstUsePos ( x)) (go xs0))
       xs}
  in go (rds d)

lastUsePos :: IntervalDesc -> Prelude.Maybe UsePos.UsePos
lastUsePos d =
  let {
   go xs =
     (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
       (\x ->
       List1.olast (Range.ups ( x)))
       (\x xs0 ->
       Maybe.option_choose (go xs0) (List1.olast (Range.ups ( x))))
       xs}
  in go (rds d)

afterLifetimeHole :: IntervalDesc -> Prelude.Int -> Prelude.Int
afterLifetimeHole d pos =
  let {
   f = \x k ->
    case (Prelude.<=) ((Prelude.succ) pos) (Range.rbeg ( x)) of {
     Prelude.True -> Range.rbeg ( x);
     Prelude.False -> k}}
  in
  let {
   go xs =
     (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
       (\x ->
       f x pos)
       (\x xs0 ->
       f x (go xs0))
       xs}
  in go (rds d)

firstUseReqReg :: IntervalDesc -> Prelude.Maybe Prelude0.Coq_oddnum
firstUseReqReg d =
  lookupUsePos d UsePos.regReq

intervalsIntersect :: IntervalDesc -> IntervalDesc -> Prelude.Maybe
                      Prelude.Int
intervalsIntersect x y =
  case (Prelude.&&) ((Prelude.<=) ((Prelude.succ) (ibeg x)) (iend y))
         ((Prelude.<=) ((Prelude.succ) (ibeg y)) (iend x)) of {
   Prelude.True -> Prelude.Just
    (case (Prelude.<=) ((Prelude.succ) (ibeg x)) (ibeg y) of {
      Prelude.True -> ibeg y;
      Prelude.False -> ibeg x});
   Prelude.False ->
    Range.rangesIntersect ( (Prelude.last (rds x))) ( (Prelude.head (rds y)))}

divideIntervalRanges :: IntervalDesc -> Prelude.Int ->
                        ((,) Range.SortedRanges Range.SortedRanges)
divideIntervalRanges d before =
  let {
   _evar_0_ = \_top_assumption_ ->
    let {
     _evar_0_ = \_top_assumption_0 ->
      let {
       _evar_0_ = \_ ->
        let {
         _evar_0_ = \_ _ ->
          let {
           _evar_0_ = \_ ->
            let {_evar_0_ = let {_evar_0_ = \_ -> (,) [] []} in  _evar_0_} in
             _evar_0_ __}
          in
           _evar_0_ __}
        in
         _evar_0_ __ __}
      in
      let {
       _evar_0_0 = \r2 rs2 ->
        let {
         _evar_0_0 = \_ ->
          let {
           _evar_0_0 = \_ _ ->
            let {
             _evar_0_0 = \_ ->
              let {
               _evar_0_0 = let {
                            _evar_0_0 = let {
                                         _evar_0_0 = \_ _ ->
                                          let {
                                           _evar_0_0 = let {
                                                        _evar_0_0 = \_ -> (,)
                                                         [] ((:) r2 rs2)}
                                                       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
           _evar_0_0 __ __}
        in
         _evar_0_0 __}
      in
      case _top_assumption_0 of {
       [] -> _evar_0_;
       (:) x x0 -> (\_ -> _evar_0_0 x x0)}}
    in
    let {
     _evar_0_0 = \r1 rs1 _top_assumption_0 ->
      let {
       _evar_0_0 = \_ ->
        let {
         _evar_0_0 = \_ _ ->
          let {
           _evar_0_0 = \_ ->
            let {
             _evar_0_0 = let {
                          _evar_0_0 = let {
                                       _evar_0_0 = \_ _ ->
                                        let {
                                         _evar_0_0 = let {
                                                      _evar_0_0 = \_ -> (,)
                                                       ((:) r1 rs1) []}
                                                     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
         _evar_0_0 __ __}
      in
      let {
       _evar_0_1 = \r2 rs2 ->
        let {
         _evar_0_1 = \_ ->
          let {
           _evar_0_1 = \_ ->
            let {
             _evar_0_1 = let {
                          _evar_0_1 = let {
                                       _evar_0_1 = \_ _ ->
                                        let {
                                         _evar_0_1 = let {
                                                      _evar_0_1 = \_ -> (,)
                                                       ((:) r1 rs1) ((:) r2
                                                       rs2)}
                                                     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
         _evar_0_1 __}
      in
      case _top_assumption_0 of {
       [] -> _evar_0_0;
       (:) x x0 -> (\_ -> _evar_0_1 x x0)}}
    in
    case _top_assumption_ of {
     [] -> _evar_0_;
     (:) x x0 -> _evar_0_0 x x0}}
  in
  case List1.span (\rd -> (Prelude.<=) (Range.rend ( rd)) before) ( (rds d)) of {
   (,) x x0 -> _evar_0_ x x0 __}

splitIntervalRanges :: IntervalDesc -> Prelude.Int ->
                       ((,) Range.SortedRanges Range.SortedRanges)
splitIntervalRanges d before =
  let {_top_assumption_ = divideIntervalRanges d before} in
  let {
   _evar_0_ = \_top_assumption_0 _top_assumption_1 ->
    let {
     _evar_0_ = \_ _ _ ->
      let {_evar_0_ = \_ -> Logic.coq_False_rec} in
      let {_evar_0_0 = \_a_ _l_ -> Logic.coq_False_rec} in
      case _top_assumption_0 of {
       [] -> _evar_0_ __;
       (:) x x0 -> _evar_0_0 x x0}}
    in
    let {
     _evar_0_0 = \r2 rs2 ->
      let {_evar_0_0 = \_ -> (,) _top_assumption_0 ((:) r2 rs2)} in
      let {
       _evar_0_1 = \_ ->
        (Prelude.flip (Prelude.$)) __ (\_ ->
          let {_top_assumption_2 = Range.rangeSpan ( r2) before} in
          let {
           _evar_0_1 = \r2a r2b -> (,) (Seq.rcons _top_assumption_0 r2a) ((:)
            r2b rs2)}
          in
          case _top_assumption_2 of {
           (,) x x0 -> _evar_0_1 x x0})}
      in
      case (Prelude.<=) before (Range.rbeg ( r2)) of {
       Prelude.True -> _evar_0_0 __;
       Prelude.False -> _evar_0_1 __}}
    in
    case _top_assumption_1 of {
     [] -> _evar_0_ __ __;
     (:) x x0 -> (\_ -> _evar_0_0 x x0)}}
  in
  case _top_assumption_ of {
   (,) x x0 -> _evar_0_ x x0 __}

type SubIntervalsOf = ((,) IntervalDesc IntervalDesc)

splitInterval :: IntervalDesc -> Prelude.Int -> SubIntervalsOf
splitInterval d before =
  let {_top_assumption_ = splitIntervalRanges d before} in
  let {
   _evar_0_ = \_top_assumption_0 ->
    let {
     _evar_0_ = \_top_assumption_1 ->
      let {_evar_0_ = \_ _ _ -> Logic.coq_False_rec} in
      let {_evar_0_0 = \r2 rs2 -> Logic.coq_False_rec} in
      case _top_assumption_1 of {
       [] -> _evar_0_ __ __;
       (:) x x0 -> (\_ -> _evar_0_0 x x0)}}
    in
    let {
     _evar_0_0 = \r1 rs1 _top_assumption_1 ->
      let {_evar_0_0 = \_ _ _ -> Logic.coq_False_rec} in
      let {
       _evar_0_1 = \r2 rs2 ->
        (Prelude.flip (Prelude.$)) __ (\_ ->
          (Prelude.flip (Prelude.$)) __ (\_ -> (,)
            (packInterval (Build_IntervalDesc (ivar (getIntervalDesc d))
              (Range.rbeg
                ( (Prelude.head (NonEmpty.coq_NE_from_list r1 rs1))))
              (Range.rend
                ( (Prelude.last (NonEmpty.coq_NE_from_list r1 rs1))))
              (NonEmpty.coq_NE_from_list r1 rs1)))
            (packInterval (Build_IntervalDesc (ivar (getIntervalDesc d))
              (Range.rbeg
                ( (Prelude.head (NonEmpty.coq_NE_from_list r2 rs2))))
              (Range.rend
                ( (Prelude.last (NonEmpty.coq_NE_from_list r2 rs2))))
              (NonEmpty.coq_NE_from_list r2 rs2)))))}
      in
      case _top_assumption_1 of {
       [] -> _evar_0_0 __ __;
       (:) x x0 -> (\_ -> _evar_0_1 x x0)}}
    in
    (\_top_assumption_1 ->
    case _top_assumption_0 of {
     [] -> _evar_0_ _top_assumption_1;
     (:) x x0 -> _evar_0_0 x x0 _top_assumption_1})}
  in
  case _top_assumption_ of {
   (,) x x0 -> _evar_0_ x x0 __}