{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- 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



#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 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}

head_or_end :: RangeDesc -> Prelude.Int
head_or_end rd =
  UsePos.head_or (rend rd) (ups rd)

getRangeDesc :: RangeDesc -> RangeDesc
getRangeDesc d =
  d

packRange :: RangeDesc -> RangeDesc
packRange d =
  d

coq_Range_shift :: RangeDesc -> Prelude.Int -> RangeDesc
coq_Range_shift rd b =
  Build_RangeDesc b (rend rd) (ups rd)

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

range_ltn :: RangeDesc -> RangeDesc -> Prelude.Bool
range_ltn x y =
  (Prelude.<=) ((Prelude.succ) (rend ( x))) (rbeg ( y))

type SortedRanges = Specif.Coq_sig2 ([] RangeDesc)

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 =
  (Prelude.||)
    (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend x))
      (unsafeCoerce (rend 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 y;
      Prelude.False -> rbeg x});
   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))

type SubRangesOf = ((,) RangeDesc RangeDesc)

rangeSpan :: RangeDesc -> Prelude.Int -> SubRangesOf
rangeSpan rd before =
  (Prelude.flip (Prelude.$)) __ (\_ ->
    case rd of {
     Build_RangeDesc rbeg0 rend0 ups0 ->
      let {
       _evar_0_ = \l1 l2 ->
        let {
         _evar_0_ = \_ _ ->
          let {
           _evar_0_ = let {
                       _evar_0_ = let {
                                   _evar_0_ = \_ ->
                                    (Prelude.flip (Prelude.$)) __ (\_ ->
                                      (Prelude.flip (Prelude.$)) __ (\_ ->
                                        (,)
                                        (packRange (Build_RangeDesc rbeg0
                                          before l1))
                                        (packRange (Build_RangeDesc before
                                          rend0 l2))))}
                                  in
                                   _evar_0_}
                      in
                       _evar_0_}
          in
           _evar_0_ __}
        in
         _evar_0_ __ __}
      in
      case Lib.span (\u ->
             (Prelude.<=) ((Prelude.succ) (UsePos.uloc u)) before) ups0 of {
       (,) x x0 -> _evar_0_ x x0}})

type BoundedRange = RangeDesc

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