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 (Typeable, Data)
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
data Range = Range { from, to :: Integer }
deriving (Eq, Ord, Show, Typeable, Data)
rangeInvariant :: Range -> Bool
rangeInvariant r = from r <= to r
overlapping :: Range -> Range -> Bool
overlapping r1 r2 = not $
to r1 <= from r2 || to r2 <= from r1
toList :: Range -> [Integer]
toList r = [from r .. to r 1]
getRanges :: C.Name -> ([Range], Bool)
getRanges n = (rToR $ P.getRange n, C.isOperator n)
getRangesA :: A.QName -> ([Range], Bool)
getRangesA = getRanges . A.nameConcrete . A.qnameName
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 }
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
tests :: IO Bool
tests = runTests "Agda.Interaction.Highlighting.Range"
[ quickCheck' rangeInvariant
]