    -- | Ranges.

    module Agda.Interaction.Highlighting.Range
      ( Range(..)
      , rangeInvariant
      , Ranges(..)
      , rangesInvariant
      , overlapping
      , overlappings
      , empty
      , rangeToPositions
      , rangesToPositions
      , rToR
      , rangeToRange
      , minus
      ) where

    import Prelude hiding (null)

    import Control.DeepSeq

    import qualified Agda.Syntax.Position as P

    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Null

    -- | Character ranges. The first character in the file has position 1.
    -- Note that the 'to' position is considered to be outside of the
    -- range.
    --
    -- Invariant: @'from' '<=' 'to'@.

    data Range = Range { Range -> Int
    from, Range -> Int
    to :: !Int }
                 deriving (Range -> Range -> Bool
    (Range -> Range -> Bool) -> (Range -> Range -> Bool) -> Eq Range
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Range -> Range -> Bool
    == :: Range -> Range -> Bool
    $c/= :: Range -> Range -> Bool
    /= :: Range -> Range -> Bool
    Eq, Eq Range
    Eq Range =>
    (Range -> Range -> Ordering)
    -> (Range -> Range -> Bool)
    -> (Range -> Range -> Bool)
    -> (Range -> Range -> Bool)
    -> (Range -> Range -> Bool)
    -> (Range -> Range -> Range)
    -> (Range -> Range -> Range)
    -> Ord Range
    Range -> Range -> Bool
    Range -> Range -> Ordering
    Range -> Range -> Range
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Range -> Range -> Ordering
    compare :: Range -> Range -> Ordering
    $c< :: Range -> Range -> Bool
    < :: Range -> Range -> Bool
    $c<= :: Range -> Range -> Bool
    <= :: Range -> Range -> Bool
    $c> :: Range -> Range -> Bool
    > :: Range -> Range -> Bool
    $c>= :: Range -> Range -> Bool
    >= :: Range -> Range -> Bool
    $cmax :: Range -> Range -> Range
    max :: Range -> Range -> Range
    $cmin :: Range -> Range -> Range
    min :: Range -> Range -> Range
    Ord, Int -> Range -> ShowS
    [Range] -> ShowS
    Range -> String
    (Int -> Range -> ShowS)
    -> (Range -> String) -> ([Range] -> ShowS) -> Show Range
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Range -> ShowS
    showsPrec :: Int -> Range -> ShowS
    $cshow :: Range -> String
    show :: Range -> String
    $cshowList :: [Range] -> ShowS
    showList :: [Range] -> ShowS
    Show)

    instance Null Range where
      empty :: Range
    empty  = Int -> Int -> Range
    Range Int
    0 Int
    0
      null :: Range -> Bool
    null Range
    r = Range -> Int
    to Range
    r Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Range -> Int
    from Range
    r

    instance NFData Range where
      rnf :: Range -> ()
    rnf (Range Int
    _ Int
    _) = ()

    -- | The 'Range' invariant.

    rangeInvariant :: Range -> Bool
    rangeInvariant :: Range -> Bool
    rangeInvariant Range
    r = Range -> Int
    from Range
    r Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Range -> Int
    to Range
    r

    -- | Zero or more consecutive and separated ranges.

    newtype Ranges = Ranges [Range]
      deriving (Ranges -> Ranges -> Bool
    (Ranges -> Ranges -> Bool)
    -> (Ranges -> Ranges -> Bool) -> Eq Ranges
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Ranges -> Ranges -> Bool
    == :: Ranges -> Ranges -> Bool
    $c/= :: Ranges -> Ranges -> Bool
    /= :: Ranges -> Ranges -> Bool
    Eq, Int -> Ranges -> ShowS
    [Ranges] -> ShowS
    Ranges -> String
    (Int -> Ranges -> ShowS)
    -> (Ranges -> String) -> ([Ranges] -> ShowS) -> Show Ranges
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Ranges -> ShowS
    showsPrec :: Int -> Ranges -> ShowS
    $cshow :: Ranges -> String
    show :: Ranges -> String
    $cshowList :: [Ranges] -> ShowS
    showList :: [Ranges] -> ShowS
    Show, Ranges -> ()
    (Ranges -> ()) -> NFData Ranges
    forall a. (a -> ()) -> NFData a
    $crnf :: Ranges -> ()
    rnf :: Ranges -> ()
    NFData)

    -- | The 'Ranges' invariant.

    rangesInvariant :: Ranges -> Bool
    rangesInvariant :: Ranges -> Bool
    rangesInvariant (Ranges [Range]
    rs) = (Range -> Range -> Bool) -> [Range] -> Bool
    forall a. (a -> a -> Bool) -> [a] -> Bool
    allConsecutive (\ Range
    r Range
    s -> Range -> Int
    to Range
    r Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Range -> Int
    from Range
    s) [Range]
    rs

    ------------------------------------------------------------------------
    -- Queries

    -- | 'True' iff the ranges overlap.
    --
    -- The ranges are assumed to be well-formed.

    overlapping :: Range -> Range -> Bool
    overlapping :: Range -> Range -> Bool
    overlapping Range
    r1 Range
    r2 = Bool -> Bool
    not (Range
    r1 Range -> Range -> Bool
    `isLeftOf` Range
    r2) Bool -> Bool -> Bool
    && Bool -> Bool
    not (Range
    r2 Range -> Range -> Bool
    `isLeftOf` Range
    r1)

    isLeftOf :: Range -> Range -> Bool
    isLeftOf :: Range -> Range -> Bool
    isLeftOf Range
    r1 Range
    r2 = Range -> Int
    to Range
    r1 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Range -> Int
    from Range
    r2

    overlappings :: Ranges -> Ranges -> Bool
    -- specification: overlappings (Ranges r1s) (Ranges r2s) = or [ overlapping r1 r2 | r1 <- r1s, r2 <- r2s ]
    overlappings :: Ranges -> Ranges -> Bool
    overlappings (Ranges [Range]
    r1s) (Ranges [Range]
    r2s) =
      Maybe [Range] -> Bool
    forall a. Maybe a -> Bool
    isNothing (Maybe [Range] -> Bool) -> Maybe [Range] -> Bool
    forall a b. (a -> b) -> a -> b
    $ (Range -> Range -> Bool) -> [Range] -> [Range] -> Maybe [Range]
    forall a. (a -> a -> Bool) -> [a] -> [a] -> Maybe [a]
    mergeStrictlyOrderedBy Range -> Range -> Bool
    isLeftOf [Range]
    r1s [Range]
    r2s

    ------------------------------------------------------------------------
    -- Conversion

    -- | Converts a range to a list of positions.

    rangeToPositions :: Range -> [Int]
    rangeToPositions :: Range -> [Int]
    rangeToPositions Range
    r = [Range -> Int
    from Range
    r .. Range -> Int
    to Range
    r Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]

    -- | Converts several ranges to a list of positions.

    rangesToPositions :: Ranges -> [Int]
    rangesToPositions :: Ranges -> [Int]
    rangesToPositions (Ranges [Range]
    rs) = (Range -> [Int]) -> [Range] -> [Int]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Range -> [Int]
    rangeToPositions [Range]
    rs

    -- | Converts a 'P.Range' to a 'Ranges'.

    rToR :: P.Range -> Ranges
    rToR :: Range -> Ranges
    rToR Range
    r = [Range] -> Ranges
    Ranges ((Interval' () -> Range) -> [Interval' ()] -> [Range]
    forall a b. (a -> b) -> [a] -> [b]
    map Interval' () -> Range
    iToR (Range -> [Interval' ()]
    forall a. Range' a -> [Interval' ()]
    P.rangeIntervals Range
    r))
      where
      iToR :: Interval' () -> Range
    iToR (P.Interval () P.Pn{ posPos :: forall a. Position' a -> Word32
    P.posPos = Word32
    pos1 } P.Pn{ posPos :: forall a. Position' a -> Word32
    P.posPos = Word32
    pos2 }) =
        Range { from :: Int
    from = Word32 -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word32
    pos1, to :: Int
    to = Word32 -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word32
    pos2 }

    -- | Converts a 'P.Range', seen as a continuous range, to a 'Range'.

    rangeToRange :: P.Range -> Range
    rangeToRange :: Range -> Range
    rangeToRange Range
    r =
      case Range -> Maybe (Interval' ())
    forall a. Range' a -> Maybe (Interval' ())
    P.rangeToInterval Range
    r of
        Maybe (Interval' ())
    Nothing -> Range { from :: Int
    from = Int
    0, to :: Int
    to = Int
    0 }
        Just (P.Interval ()
    _ Position' ()
    s Position' ()
    e) -> Range
          { from :: Int
    from = Word32 -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Word32 -> Int) -> Word32 -> Int
    forall a b. (a -> b) -> a -> b
    $ Position' () -> Word32
    forall a. Position' a -> Word32
    P.posPos Position' ()
    s
          , to :: Int
    to   = Word32 -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Word32 -> Int) -> Word32 -> Int
    forall a b. (a -> b) -> a -> b
    $ Position' () -> Word32
    forall a. Position' a -> Word32
    P.posPos Position' ()
    e
          }

    ------------------------------------------------------------------------
    -- Operations

    -- | @minus xs ys@ computes the difference between @xs@ and @ys@: the
    -- result contains those positions which are present in @xs@ but not
    -- in @ys@.
    --
    -- Linear in the lengths of the input ranges.

    minus :: Ranges -> Ranges -> Ranges
    minus :: Ranges -> Ranges -> Ranges
    minus (Ranges [Range]
    rs1) (Ranges [Range]
    rs2) = [Range] -> Ranges
    Ranges ([Range] -> [Range] -> [Range]
    m [Range]
    rs1 [Range]
    rs2)
      where
      m :: [Range] -> [Range] -> [Range]
    m []     [Range]
    _      = []
      m [Range]
    xs     []     = [Range]
    xs
      m (Range
    x:[Range]
    xs) (Range
    y:[Range]
    ys)
        | Range -> Bool
    forall a. Null a => a -> Bool
    null Range
    y          = [Range] -> [Range] -> [Range]
    m (Range
    xRange -> [Range] -> [Range]
    forall a. a -> [a] -> [a]
    :[Range]
    xs) [Range]
    ys
        | Range -> Int
    to Range
    x Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Range -> Int
    from Range
    y   = Range
    x Range -> [Range] -> [Range]
    forall a. a -> [a] -> [a]
    : [Range] -> [Range] -> [Range]
    m [Range]
    xs (Range
    yRange -> [Range] -> [Range]
    forall a. a -> [a] -> [a]
    :[Range]
    ys)
        | Range -> Int
    to Range
    y Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Range -> Int
    from Range
    x   = [Range] -> [Range] -> [Range]
    m (Range
    xRange -> [Range] -> [Range]
    forall a. a -> [a] -> [a]
    :[Range]
    xs) [Range]
    ys
        | Range -> Int
    from Range
    x Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Range -> Int
    from Range
    y = Range { from :: Int
    from = Range -> Int
    from Range
    x, to :: Int
    to = Range -> Int
    from Range
    y } Range -> [Range] -> [Range]
    forall a. a -> [a] -> [a]
    :
                            [Range] -> [Range] -> [Range]
    m (Range { from :: Int
    from = Range -> Int
    from Range
    y, to :: Int
    to = Range -> Int
    to Range
    x } Range -> [Range] -> [Range]
    forall a. a -> [a] -> [a]
    : [Range]
    xs) (Range
    yRange -> [Range] -> [Range]
    forall a. a -> [a] -> [a]
    :[Range]
    ys)
        | Range -> Int
    to Range
    y Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Range -> Int
    to Range
    x     = [Range] -> [Range] -> [Range]
    m (Range { from :: Int
    from = Range -> Int
    to Range
    y, to :: Int
    to = Range -> Int
    to Range
    x } Range -> [Range] -> [Range]
    forall a. a -> [a] -> [a]
    : [Range]
    xs) [Range]
    ys
        | Bool
    otherwise       = [Range] -> [Range] -> [Range]
    m [Range]
    xs (Range
    yRange -> [Range] -> [Range]
    forall a. a -> [a] -> [a]
    :[Range]
    ys)