-- | 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Range -> Range -> Bool
$c/= :: Range -> Range -> Bool
== :: Range -> Range -> Bool
$c== :: Range -> Range -> Bool
Eq, Eq 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
min :: Range -> Range -> Range
$cmin :: Range -> Range -> Range
max :: Range -> Range -> Range
$cmax :: Range -> Range -> Range
>= :: Range -> Range -> Bool
$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
compare :: Range -> Range -> Ordering
$ccompare :: Range -> Range -> Ordering
Ord, Int -> Range -> ShowS
[Range] -> ShowS
Range -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Range] -> ShowS
$cshowList :: [Range] -> ShowS
show :: Range -> String
$cshow :: Range -> String
showsPrec :: Int -> Range -> ShowS
$cshowsPrec :: Int -> 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 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 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ranges -> Ranges -> Bool
$c/= :: Ranges -> Ranges -> Bool
== :: Ranges -> Ranges -> Bool
$c== :: Ranges -> Ranges -> Bool
Eq, Int -> Ranges -> ShowS
[Ranges] -> ShowS
Ranges -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ranges] -> ShowS
$cshowList :: [Ranges] -> ShowS
show :: Ranges -> String
$cshow :: Ranges -> String
showsPrec :: Int -> Ranges -> ShowS
$cshowsPrec :: Int -> Ranges -> ShowS
Show, Ranges -> ()
forall a. (a -> ()) -> NFData a
rnf :: Ranges -> ()
$crnf :: Ranges -> ()
NFData)

-- | The 'Ranges' invariant.

rangesInvariant :: Ranges -> Bool
rangesInvariant :: Ranges -> Bool
rangesInvariant (Ranges []) = Bool
True
rangesInvariant (Ranges [Range]
rs) =
  forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. Ord a => a -> a -> Bool
(<) (forall a b. (a -> b) -> [a] -> [b]
map Range -> Int
to forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
init [Range]
rs) (forall a b. (a -> b) -> [a] -> [b]
map Range -> Int
from forall a b. (a -> b) -> a -> b
$ forall a. [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 forall a b. (a -> b) -> a -> b
$ Range
r1 Range -> Range -> Bool
`isLeftOf` Range
r2) Bool -> Bool -> Bool
&& (Bool -> Bool
not 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 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) =
  forall a. Maybe a -> Bool
isNothing forall a b. (a -> b) -> a -> b
$ 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 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) = 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 (forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Interval' a -> Range
iToR (forall a. Range' a -> [IntervalWithoutFile]
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 = forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
pos1, to :: Int
to = 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 forall a. Range' a -> Maybe IntervalWithoutFile
P.rangeToInterval Range
r of
    Maybe IntervalWithoutFile
Nothing -> Range { from :: Int
from = Int
0, to :: Int
to = Int
0 }
    Just IntervalWithoutFile
i  -> Range { from :: Int
from = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall a. Position' a -> Int32
P.posPos forall a b. (a -> b) -> a -> b
$ forall a. Interval' a -> Position' a
P.iStart IntervalWithoutFile
i
                     , to :: Int
to   = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall a. Position' a -> Int32
P.posPos forall a b. (a -> b) -> a -> b
$ forall a. Interval' a -> Position' a
P.iEnd IntervalWithoutFile
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)
    | forall a. Null a => a -> Bool
null Range
y          = [Range] -> [Range] -> [Range]
m (Range
xforall a. a -> [a] -> [a]
:[Range]
xs) [Range]
ys
    | Range -> Int
to Range
x forall a. Ord a => a -> a -> Bool
< Range -> Int
from Range
y   = Range
x forall a. a -> [a] -> [a]
: [Range] -> [Range] -> [Range]
m [Range]
xs (Range
yforall a. a -> [a] -> [a]
:[Range]
ys)
    | Range -> Int
to Range
y forall a. Ord a => a -> a -> Bool
< Range -> Int
from Range
x   = [Range] -> [Range] -> [Range]
m (Range
xforall a. a -> [a] -> [a]
:[Range]
xs) [Range]
ys
    | Range -> Int
from Range
x 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 } 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 } forall a. a -> [a] -> [a]
: [Range]
xs) (Range
yforall a. a -> [a] -> [a]
:[Range]
ys)
    | Range -> Int
to Range
y 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 } forall a. a -> [a] -> [a]
: [Range]
xs) [Range]
ys
    | Bool
otherwise       = [Range] -> [Range] -> [Range]
m [Range]
xs (Range
yforall a. a -> [a] -> [a]
:[Range]
ys)