    {-# LANGUAGE DeriveDataTypeable #-}

    -- | Ranges.

    module Agda.Interaction.Highlighting.Range
      ( Range(..)
      , rangeInvariant
      , overlapping
      , toList
      , getRanges
      , getRangesA
      , rToR
      , Agda.Interaction.Highlighting.Range.tests
      ) where

    import Agda.Utils.QuickCheck
    import Data.List
    import Data.Generics
    import Agda.Utils.TestHelpers
    import qualified Agda.Syntax.Abstract as A
    import qualified Agda.Syntax.Concrete as C
    import qualified Agda.Syntax.Position as P

    -- | 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 :: Integer }
                 deriving (Eq, Ord, Show, Typeable, Data)

    -- | The 'Range' invariant.

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

    -- | '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

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

    toList :: Range -> [Integer]
    toList r = [from r .. to r - 1]

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

    -- | Calculates a set of ranges associated with a name.
    --
    -- For an operator the ranges associated with the NameParts are
    -- returned. Otherwise the range associated with the Name is returned.
    --
    -- A boolean, indicating operatorness, is also returned.

    getRanges :: C.Name -> ([Range], Bool)
    getRanges n = (rToR $ P.getRange n, C.isOperator n)

    -- | Like 'getRanges', but for 'A.QName's. Note that the module part
    -- of the name is thrown away; only the base part is used.

    getRangesA :: A.QName -> ([Range], Bool)
    getRangesA = getRanges . A.nameConcrete . A.qnameName

    -- | Converts a 'P.Range' to a list of 'Range's.

    rToR :: P.Range -> [Range]
    rToR (P.Range is) = map iToR is
      where
      iToR (P.Interval { P.iStart = P.Pn { P.posPos = pos1 }
                       , P.iEnd   = P.Pn { P.posPos = pos2 }
                       }) =
        Range { from = toInteger pos1, to = toInteger pos2 }

    ------------------------------------------------------------------------
    -- Generators

    instance Arbitrary Range where
      arbitrary = do
        [from, to] <- fmap sort $ vectorOf 2 positive
        return $ Range { from = from, to = to }

    instance CoArbitrary Range where
      coarbitrary (Range f t) = coarbitrary f . coarbitrary t

    ------------------------------------------------------------------------
    -- All tests

    -- | All the properties.

    tests :: IO Bool
    tests = runTests "Agda.Interaction.Highlighting.Range"
      [ quickCheck' rangeInvariant
      ]