-- | Ranges.

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

-- | 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 { 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
_) = ()

-- | The 'Range' invariant.

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

-- | Zero or more consecutive and separated ranges.

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)

-- | The 'Ranges' invariant.

rangesInvariant :: Ranges -> Bool
rangesInvariant :: Ranges -> Bool
rangesInvariant (Ranges []) = Bool
True
rangesInvariant (Ranges [Range]
rs) =
  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Int -> Int -> Bool) -> [Int] -> [Int] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
(<) ((Range -> Int) -> [Range] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Int
to ([Range] -> [Int]) -> [Range] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Range] -> [Range]
forall a. HasCallStack => [a] -> [a]
init [Range]
rs) ((Range -> Int) -> [Range] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Int
from ([Range] -> [Int]) -> [Range] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Range] -> [Range]
forall a. HasCallStack => [a] -> [a]
tail [Range]
rs))

------------------------------------------------------------------------
-- Queries

-- | 'True' iff the ranges overlap.
--
-- The ranges are assumed to be well-formed.

overlapping :: Range -> Range -> Bool
overlapping :: Range -> Range -> Bool
overlapping Range
r1 Range
r2 = (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Range
r1 Range -> Range -> Bool
`isLeftOf` Range
r2) Bool -> Bool -> Bool
&& (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ 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
-- specification: overlappings (Ranges r1s) (Ranges r2s) = or [ overlapping r1 r2 | r1 <- r1s, r2 <- r2s ]
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

------------------------------------------------------------------------
-- Conversion

-- | Converts a range to a list of positions.

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]

-- | Converts several ranges to a list of positions.

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

-- | Converts a 'P.Range' to a 'Ranges'.

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 }

-- | Converts a 'P.Range', seen as a continuous range, to a 'Range'.

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
                     }

------------------------------------------------------------------------
-- 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 -> 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)