{-# LANGUAGE DeriveDataTypeable #-}
-- | Ranges.
module Agda.Interaction.Highlighting.Range
( Range(..)
, rangeInvariant
, Ranges(..)
, rangesInvariant
, overlapping
, empty
, rangeToPositions
, rangesToPositions
, rToR
, rangeToEndPoints
, 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 :: Int }
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 -> [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
prop_rangesToPositions :: Ranges -> Bool
prop_rangesToPositions rs = sorted (rangesToPositions 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)
prop_minus :: Ranges -> Ranges -> Bool
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
]