module Agda.Interaction.Highlighting.Range
( Range(..)
, rangeInvariant
, Ranges(..)
, rangesInvariant
, overlapping
, overlappings
, empty
, rangeToPositions
, rangesToPositions
, rToR
, rangeToRange
, minus
) where
import Prelude hiding (null)
import Control.DeepSeq
import qualified Agda.Syntax.Position as P
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Null
data Range = Range { Range -> Int
from, Range -> Int
to :: !Int }
deriving (Range -> Range -> Bool
(Range -> Range -> Bool) -> (Range -> Range -> Bool) -> Eq Range
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Range -> Range -> Bool
== :: Range -> Range -> Bool
$c/= :: Range -> Range -> Bool
/= :: Range -> Range -> Bool
Eq, Eq Range
Eq Range =>
(Range -> Range -> Ordering)
-> (Range -> Range -> Bool)
-> (Range -> Range -> Bool)
-> (Range -> Range -> Bool)
-> (Range -> Range -> Bool)
-> (Range -> Range -> Range)
-> (Range -> Range -> Range)
-> Ord Range
Range -> Range -> Bool
Range -> Range -> Ordering
Range -> Range -> Range
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Range -> Range -> Ordering
compare :: Range -> Range -> Ordering
$c< :: Range -> Range -> Bool
< :: Range -> Range -> Bool
$c<= :: Range -> Range -> Bool
<= :: Range -> Range -> Bool
$c> :: Range -> Range -> Bool
> :: Range -> Range -> Bool
$c>= :: Range -> Range -> Bool
>= :: Range -> Range -> Bool
$cmax :: Range -> Range -> Range
max :: Range -> Range -> Range
$cmin :: Range -> Range -> Range
min :: Range -> Range -> Range
Ord, Int -> Range -> ShowS
[Range] -> ShowS
Range -> String
(Int -> Range -> ShowS)
-> (Range -> String) -> ([Range] -> ShowS) -> Show Range
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Range -> ShowS
showsPrec :: Int -> Range -> ShowS
$cshow :: Range -> String
show :: Range -> String
$cshowList :: [Range] -> ShowS
showList :: [Range] -> ShowS
Show)
instance Null Range where
empty :: Range
empty = Int -> Int -> Range
Range Int
0 Int
0
null :: Range -> Bool
null Range
r = Range -> Int
to Range
r Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Range -> Int
from Range
r
instance NFData Range where
rnf :: Range -> ()
rnf (Range Int
_ Int
_) = ()
rangeInvariant :: Range -> Bool
rangeInvariant :: Range -> Bool
rangeInvariant Range
r = Range -> Int
from Range
r Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Range -> Int
to Range
r
newtype Ranges = Ranges [Range]
deriving (Ranges -> Ranges -> Bool
(Ranges -> Ranges -> Bool)
-> (Ranges -> Ranges -> Bool) -> Eq Ranges
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Ranges -> Ranges -> Bool
== :: Ranges -> Ranges -> Bool
$c/= :: Ranges -> Ranges -> Bool
/= :: Ranges -> Ranges -> Bool
Eq, Int -> Ranges -> ShowS
[Ranges] -> ShowS
Ranges -> String
(Int -> Ranges -> ShowS)
-> (Ranges -> String) -> ([Ranges] -> ShowS) -> Show Ranges
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Ranges -> ShowS
showsPrec :: Int -> Ranges -> ShowS
$cshow :: Ranges -> String
show :: Ranges -> String
$cshowList :: [Ranges] -> ShowS
showList :: [Ranges] -> ShowS
Show, Ranges -> ()
(Ranges -> ()) -> NFData Ranges
forall a. (a -> ()) -> NFData a
$crnf :: Ranges -> ()
rnf :: Ranges -> ()
NFData)
rangesInvariant :: Ranges -> Bool
rangesInvariant :: Ranges -> Bool
rangesInvariant (Ranges [Range]
rs) = (Range -> Range -> Bool) -> [Range] -> Bool
forall a. (a -> a -> Bool) -> [a] -> Bool
allConsecutive (\ Range
r Range
s -> Range -> Int
to Range
r Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Range -> Int
from Range
s) [Range]
rs
overlapping :: Range -> Range -> Bool
overlapping :: Range -> Range -> Bool
overlapping Range
r1 Range
r2 = Bool -> Bool
not (Range
r1 Range -> Range -> Bool
`isLeftOf` Range
r2) Bool -> Bool -> Bool
&& Bool -> Bool
not (Range
r2 Range -> Range -> Bool
`isLeftOf` Range
r1)
isLeftOf :: Range -> Range -> Bool
isLeftOf :: Range -> Range -> Bool
isLeftOf Range
r1 Range
r2 = Range -> Int
to Range
r1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Range -> Int
from Range
r2
overlappings :: Ranges -> Ranges -> Bool
overlappings :: Ranges -> Ranges -> Bool
overlappings (Ranges [Range]
r1s) (Ranges [Range]
r2s) =
Maybe [Range] -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe [Range] -> Bool) -> Maybe [Range] -> Bool
forall a b. (a -> b) -> a -> b
$ (Range -> Range -> Bool) -> [Range] -> [Range] -> Maybe [Range]
forall a. (a -> a -> Bool) -> [a] -> [a] -> Maybe [a]
mergeStrictlyOrderedBy Range -> Range -> Bool
isLeftOf [Range]
r1s [Range]
r2s
rangeToPositions :: Range -> [Int]
rangeToPositions :: Range -> [Int]
rangeToPositions Range
r = [Range -> Int
from Range
r .. Range -> Int
to Range
r Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
rangesToPositions :: Ranges -> [Int]
rangesToPositions :: Ranges -> [Int]
rangesToPositions (Ranges [Range]
rs) = (Range -> [Int]) -> [Range] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Range -> [Int]
rangeToPositions [Range]
rs
rToR :: P.Range -> Ranges
rToR :: Range -> Ranges
rToR Range
r = [Range] -> Ranges
Ranges ((Interval' () -> Range) -> [Interval' ()] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map Interval' () -> Range
forall {a}. Interval' a -> Range
iToR (Range -> [Interval' ()]
forall a. Range' a -> [Interval' ()]
P.rangeIntervals Range
r))
where
iToR :: Interval' a -> Range
iToR (P.Interval { iStart :: forall a. Interval' a -> Position' a
P.iStart = P.Pn { posPos :: forall a. Position' a -> Int32
P.posPos = Int32
pos1 }
, iEnd :: forall a. Interval' a -> Position' a
P.iEnd = P.Pn { posPos :: forall a. Position' a -> Int32
P.posPos = Int32
pos2 }
}) =
Range { from :: Int
from = Int32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
pos1, to :: Int
to = Int32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
pos2 }
rangeToRange :: P.Range -> Range
rangeToRange :: Range -> Range
rangeToRange Range
r =
case Range -> Maybe (Interval' ())
forall a. Range' a -> Maybe (Interval' ())
P.rangeToInterval Range
r of
Maybe (Interval' ())
Nothing -> Range { from :: Int
from = Int
0, to :: Int
to = Int
0 }
Just Interval' ()
i -> Range { from :: Int
from = Int32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> Int) -> Int32 -> Int
forall a b. (a -> b) -> a -> b
$ Position' () -> Int32
forall a. Position' a -> Int32
P.posPos (Position' () -> Int32) -> Position' () -> Int32
forall a b. (a -> b) -> a -> b
$ Interval' () -> Position' ()
forall a. Interval' a -> Position' a
P.iStart Interval' ()
i
, to :: Int
to = Int32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> Int) -> Int32 -> Int
forall a b. (a -> b) -> a -> b
$ Position' () -> Int32
forall a. Position' a -> Int32
P.posPos (Position' () -> Int32) -> Position' () -> Int32
forall a b. (a -> b) -> a -> b
$ Interval' () -> Position' ()
forall a. Interval' a -> Position' a
P.iEnd Interval' ()
i
}
minus :: Ranges -> Ranges -> Ranges
minus :: Ranges -> Ranges -> Ranges
minus (Ranges [Range]
rs1) (Ranges [Range]
rs2) = [Range] -> Ranges
Ranges ([Range] -> [Range] -> [Range]
m [Range]
rs1 [Range]
rs2)
where
m :: [Range] -> [Range] -> [Range]
m [] [Range]
_ = []
m [Range]
xs [] = [Range]
xs
m (Range
x:[Range]
xs) (Range
y:[Range]
ys)
| Range -> Bool
forall a. Null a => a -> Bool
null Range
y = [Range] -> [Range] -> [Range]
m (Range
xRange -> [Range] -> [Range]
forall a. a -> [a] -> [a]
:[Range]
xs) [Range]
ys
| Range -> Int
to Range
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Range -> Int
from Range
y = Range
x Range -> [Range] -> [Range]
forall a. a -> [a] -> [a]
: [Range] -> [Range] -> [Range]
m [Range]
xs (Range
yRange -> [Range] -> [Range]
forall a. a -> [a] -> [a]
:[Range]
ys)
| Range -> Int
to Range
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Range -> Int
from Range
x = [Range] -> [Range] -> [Range]
m (Range
xRange -> [Range] -> [Range]
forall a. a -> [a] -> [a]
:[Range]
xs) [Range]
ys
| Range -> Int
from Range
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Range -> Int
from Range
y = Range { from :: Int
from = Range -> Int
from Range
x, to :: Int
to = Range -> Int
from Range
y } Range -> [Range] -> [Range]
forall a. a -> [a] -> [a]
:
[Range] -> [Range] -> [Range]
m (Range { from :: Int
from = Range -> Int
from Range
y, to :: Int
to = Range -> Int
to Range
x } Range -> [Range] -> [Range]
forall a. a -> [a] -> [a]
: [Range]
xs) (Range
yRange -> [Range] -> [Range]
forall a. a -> [a] -> [a]
:[Range]
ys)
| Range -> Int
to Range
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Range -> Int
to Range
x = [Range] -> [Range] -> [Range]
m (Range { from :: Int
from = Range -> Int
to Range
y, to :: Int
to = Range -> Int
to Range
x } Range -> [Range] -> [Range]
forall a. a -> [a] -> [a]
: [Range]
xs) [Range]
ys
| Bool
otherwise = [Range] -> [Range] -> [Range]
m [Range]
xs (Range
yRange -> [Range] -> [Range]
forall a. a -> [a] -> [a]
:[Range]
ys)