{-# LANGUAGE DeriveDataTypeable #-}

-- | Ranges.

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

import Control.Applicative ((<$>))
import Data.List
import Data.Typeable (Typeable)

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

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

-- | 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 -> [Integer]
rangeToPositions r = [from r .. to r - 1]

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

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

prop_rangesToPositions rs = sorted (rangesToPositions rs)

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

rToR :: P.Range -> Ranges
rToR (P.Range is) = Ranges (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 }

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

prop_minus xs ys =
  rangesToPositions (xs `minus` ys) ==
  rangesToPositions xs \\ rangesToPositions ys

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

instance Arbitrary Ranges where
  arbitrary = rToR <$> arbitrary

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

-- | All the properties.

tests :: IO Bool
tests = runTests "Agda.Interaction.Highlighting.Range"
  [ quickCheck' rangeInvariant
  , quickCheck' rangesInvariant
  , quickCheck' (rangesInvariant . rToR)
  , quickCheck' (\r1 r2 -> rangesInvariant $ r1 `minus` r2)
  , quickCheck' prop_rangesToPositions
  , quickCheck' prop_minus
  ]