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

module LinearScan.Range 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.Datatypes as Datatypes
import qualified LinearScan.Lib as Lib
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



--unsafeCoerce :: a -> b
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base as GHC.Base
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
import qualified LinearScan.IOExts as IOExts
unsafeCoerce = IOExts.unsafeCoerce
#endif

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

data RangeDesc =
   Build_RangeDesc Prelude.Int Prelude.Int ([] UsePos.UsePos)

rbeg :: RangeDesc -> Prelude.Int
rbeg r =
  case r of {
   Build_RangeDesc rbeg0 rend0 ups0 -> rbeg0}

rend :: RangeDesc -> Prelude.Int
rend r =
  case r of {
   Build_RangeDesc rbeg0 rend0 ups0 -> rend0}

ups :: RangeDesc -> [] UsePos.UsePos
ups r =
  case r of {
   Build_RangeDesc rbeg0 rend0 ups0 -> ups0}

getRangeDesc :: RangeDesc -> RangeDesc
getRangeDesc d =
  d

packRange :: RangeDesc -> RangeDesc
packRange d =
  d

newRange :: UsePos.UsePos -> RangeDesc
newRange upos =
  Build_RangeDesc (UsePos.uloc upos) ((Prelude.succ) (UsePos.uloc upos)) ((:)
    upos [])

coq_Range_cons :: UsePos.UsePos -> RangeDesc -> RangeDesc
coq_Range_cons upos rd =
  Build_RangeDesc (rbeg rd) (rend rd) ((:) upos (ups rd))

type BoundedRange = RangeDesc

emptyBoundedRange :: Prelude.Int -> Prelude.Int -> BoundedRange
emptyBoundedRange b e =
  Build_RangeDesc b e []

type SortedRanges = Specif.Coq_sig2 ([] RangeDesc)

emptySortedRanges :: Prelude.Int -> SortedRanges
emptySortedRanges b =
  []

prependRange :: Prelude.Int -> Prelude.Int -> BoundedRange -> SortedRanges ->
                Prelude.Int -> SortedRanges
prependRange b e rp ranges pos =
  let {_evar_0_ = \_ _ -> (:) rp []} in
  let {
   _evar_0_0 = \x xs ->
    let {
     _evar_0_0 = \_ _ ->
      let {
       r' = packRange (Build_RangeDesc (rbeg (getRangeDesc ( rp)))
              (rend (getRangeDesc ( x)))
              ((Prelude.++) (ups (getRangeDesc ( rp)))
                (ups (getRangeDesc ( x)))))}
      in
      (:) r' xs}
    in
    let {_evar_0_1 = \_ _ -> (:) rp ((:) x xs)} in
    case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend ( rp)))
           (unsafeCoerce (rbeg ( x))) of {
     Prelude.True -> _evar_0_0 __ __;
     Prelude.False -> _evar_0_1 __ __}}
  in
  case ranges of {
   [] -> _evar_0_ __ __;
   (:) x x0 -> _evar_0_0 x x0}

coq_SortedRanges_cat :: Prelude.Int -> SortedRanges -> Prelude.Int ->
                        SortedRanges -> SortedRanges
coq_SortedRanges_cat b xs pos ys =
  let {
   _evar_0_ = \_ _ _ ->
    let {_evar_0_ = \_ _ _ -> []} in
    let {_evar_0_0 = \r rs -> (:) r rs} in
    case ys of {
     [] -> _evar_0_ __ __ __;
     (:) x x0 -> _evar_0_0 x x0}}
  in
  let {
   _evar_0_0 = \ps p ->
    let {_evar_0_0 = \_ _ _ -> Seq.rcons ps p} in
    let {
     _evar_0_1 = \r rs ->
      let {
       _evar_0_1 = \_ ->
        let {
         r' = packRange (Build_RangeDesc (rbeg (getRangeDesc ( p)))
                (rend (getRangeDesc ( r)))
                ((Prelude.++) (ups (getRangeDesc ( p)))
                  (ups (getRangeDesc ( r)))))}
        in
        (Prelude.++) ps ((:) r' rs)}
      in
      let {_evar_0_2 = \_ -> (Prelude.++) (Seq.rcons ps p) ((:) r rs)} in
      case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend ( p)))
             (unsafeCoerce (rbeg ( r))) of {
       Prelude.True -> _evar_0_1 __;
       Prelude.False -> _evar_0_2 __}}
    in
    case ys of {
     [] -> _evar_0_0 __ __ __;
     (:) x x0 -> _evar_0_1 x x0}}
  in
  case Seq.lastP xs of {
   Seq.LastNil -> _evar_0_ __ __ __;
   Seq.LastRcons x x0 -> _evar_0_0 x x0}

transportSortedRanges :: Prelude.Int -> Prelude.Int -> SortedRanges ->
                         SortedRanges
transportSortedRanges b pos rp =
  rp

rangesIntersect :: RangeDesc -> RangeDesc -> Prelude.Bool
rangesIntersect x y =
  case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of {
   Prelude.True -> (Prelude.<=) ((Prelude.succ) (rbeg y)) (rend x);
   Prelude.False -> (Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y)}

rangeIntersectionPoint :: RangeDesc -> RangeDesc -> Prelude.Maybe
                          Lib.Coq_oddnum
rangeIntersectionPoint x y =
  case rangesIntersect x y of {
   Prelude.True -> Prelude.Just
    (case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of {
      Prelude.True -> rbeg x;
      Prelude.False -> rbeg y});
   Prelude.False -> Prelude.Nothing}

findRangeUsePos :: RangeDesc -> (UsePos.UsePos -> Prelude.Bool) ->
                   Prelude.Maybe UsePos.UsePos
findRangeUsePos rd f =
  let {_evar_0_ = Prelude.Nothing} in
  let {
   _evar_0_0 = \u us iHxs ->
    let {_evar_0_0 = Prelude.Just u} in
    let {
     _evar_0_1 = let {
                  _evar_0_1 = \_top_assumption_ -> Prelude.Just
                   _top_assumption_}
                 in
                 let {_evar_0_2 = Prelude.Nothing} in
                 case iHxs of {
                  Prelude.Just x -> _evar_0_1 x;
                  Prelude.Nothing -> _evar_0_2}}
    in
    case f u of {
     Prelude.True -> _evar_0_0;
     Prelude.False -> _evar_0_1}}
  in
  Datatypes.list_rec _evar_0_ _evar_0_0 (ups (getRangeDesc rd))

rangeSpan :: Prelude.Int -> RangeDesc ->
             ((,) (Prelude.Maybe RangeDesc) (Prelude.Maybe RangeDesc))
rangeSpan before rd =
  (Prelude.flip (Prelude.$)) __ (\_ ->
    case rd of {
     Build_RangeDesc rbeg0 rend0 ups0 ->
      let {
       _evar_0_ = \l1 l2 ->
        let {
         _evar_0_ = \_ ->
          let {
           _evar_0_ = \_ -> (,) Prelude.Nothing (Prelude.Just
            (packRange (Build_RangeDesc rbeg0 rend0 ((Prelude.++) l1 l2))))}
          in
          let {
           _evar_0_0 = \_ ->
            let {
             _evar_0_0 = \_ -> (,) (Prelude.Just
              (packRange (Build_RangeDesc rbeg0 rend0 ((Prelude.++) l1 l2))))
              Prelude.Nothing}
            in
            let {
             _evar_0_1 = \_ ->
              let {
               _evar_0_1 = \_ ->
                let {
                 _evar_0_1 = \_ ->
                  (Prelude.flip (Prelude.$)) __ (\_ ->
                    let {
                     _evar_0_1 = \_ _ _ _ -> (,) (Prelude.Just
                      (packRange (Build_RangeDesc rbeg0 before l1)))
                      Prelude.Nothing}
                    in
                    let {
                     _evar_0_2 = \u us ->
                      (Prelude.flip (Prelude.$)) __ (\_ -> (,) (Prelude.Just
                        (packRange (Build_RangeDesc rbeg0 before l1)))
                        (Prelude.Just
                        (packRange (Build_RangeDesc (UsePos.uloc u) rend0
                          ((:) u us)))))}
                    in
                    case l2 of {
                     [] -> _evar_0_1 __ __ __ __;
                     (:) x x0 -> _evar_0_2 x x0})}
                in
                 _evar_0_1 __}
              in
               _evar_0_1 __}
            in
            case (Prelude.<=) rend0 before of {
             Prelude.True -> _evar_0_0 __;
             Prelude.False -> _evar_0_1 __}}
          in
          case (Prelude.<=) before rbeg0 of {
           Prelude.True -> _evar_0_ __;
           Prelude.False -> _evar_0_0 __}}
        in
         _evar_0_ __}
      in
      case Lib.span (\x ->
             (Prelude.<=) ((Prelude.succ) (UsePos.uloc x)) before) ups0 of {
       (,) x x0 -> _evar_0_ x x0}})