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
data Range = Range { from, to :: Int }
deriving (Eq, Ord, Show, Typeable)
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
prop_rangesToPositions :: Ranges -> Bool
prop_rangesToPositions rs = sorted (rangesToPositions rs)
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 = fromIntegral pos1, to = fromIntegral pos2 }
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
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
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
]