    {-# LANGUAGE DeriveDataTypeable #-}

    -- | Ranges.

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

    import Control.Applicative ((<$>))

    import qualified Agda.Syntax.Position as P
    import Agda.Utils.List

    -- | 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 { from, to :: Int }
                 deriving (Eq, Ord, Show)

    -- | The 'Range' invariant.

    rangeInvariant :: Range -> Bool
    rangeInvariant r = from r <= to r

    -- | Zero or more consecutive and separated ranges.

    newtype Ranges = Ranges [Range]
      deriving (Eq, Show)

    -- | The 'Ranges' invariant.

    rangesInvariant :: Ranges -> Bool
    rangesInvariant (Ranges []) = True
    rangesInvariant (Ranges rs) =
      and (zipWith (<) (map to $ init rs) (map from $ tail rs))

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

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

    overlapping :: Range -> Range -> Bool
    overlapping r1 r2 = not $
      to r1 <= from r2 || to r2 <= from r1

    -- | 'True' iff the range is empty.

    empty :: Range -> Bool
    empty r = to r <= from r

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

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

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

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

    rangesToPositions :: Ranges -> [Int]
    rangesToPositions (Ranges rs) = concatMap rangeToPositions rs

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

    rToR :: P.Range -> Ranges
    rToR r = Ranges (map iToR (P.rangeIntervals r))
      where
      iToR (P.Interval { P.iStart = P.Pn { P.posPos = pos1 }
                       , P.iEnd   = P.Pn { P.posPos = pos2 }
                       }) =
        Range { from = fromIntegral pos1, to = fromIntegral pos2 }

    rangeToEndPoints :: P.Range -> Maybe (Int,Int)
    rangeToEndPoints r =
      case P.rangeToInterval r of
              Nothing -> Nothing
              Just i  -> Just ( fromIntegral $ P.posPos $ P.iStart i
                              , fromIntegral $ P.posPos $ P.iEnd i)

    ------------------------------------------------------------------------
    -- 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 rs1) (Ranges rs2) = Ranges (m rs1 rs2)
      where
      m []     _      = []
      m xs     []     = xs
      m (x:xs) (y:ys)
        | empty y         = m (x:xs) ys
        | to x < from y   = x : m xs (y:ys)
        | to y < from x   = m (x:xs) ys
        | from x < from y = Range { from = from x, to = from y } :
                            m (Range { from = from y, to = to x } : xs) (y:ys)
        | to y < to x     = m (Range { from = to y, to = to x } : xs) ys
        | otherwise       = m xs (y:ys)