{-# LANGUAGE DeriveDataTypeable #-}
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
data Range = Range { from, to :: Int }
deriving (Eq, Ord, Show)
rangeInvariant :: Range -> Bool
rangeInvariant r = from r <= to r
newtype Ranges = Ranges [Range]
deriving (Eq, Show)
rangesInvariant :: Ranges -> Bool
rangesInvariant (Ranges []) = True
rangesInvariant (Ranges rs) =
and (zipWith (<) (map to $ init rs) (map from $ tail rs))
overlapping :: Range -> Range -> Bool
overlapping r1 r2 = not $
to r1 <= from r2 || to r2 <= from r1
empty :: Range -> Bool
empty r = to r <= from r
rangeToPositions :: Range -> [Int]
rangeToPositions r = [from r .. to r - 1]
rangesToPositions :: Ranges -> [Int]
rangesToPositions (Ranges rs) = concatMap rangeToPositions rs
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)
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)