{- |
Module: Agda.Unused.Types.Range

Location ranges of Agda code files.
-}
module Agda.Unused.Types.Range

  ( -- * Definitions

    Range
  , Range'(..)
  , RangeType(..)
  , RangeInfo(..)

    -- * Interface

  , getRange
  , rangePath
  , rangeContains

  ) where

import Agda.Unused.Types.Name
  (QName)

import Agda.Syntax.Position
  (PositionWithoutFile, Range, Range'(..), getRange, rEnd', rStart')
import Agda.Utils.FileName
  (filePath)
import qualified Agda.Utils.Maybe.Strict
  as S

-- ## Definitions

-- | The type of item found at a named range.
data RangeType where

  RangeData
    :: RangeType

  RangeDefinition
    :: RangeType

  RangeImport
    :: RangeType

  RangeImportItem
    :: RangeType

  RangeModule
    :: RangeType

  RangeModuleItem
    :: RangeType

  RangeOpen
    :: RangeType

  RangeOpenItem
    :: RangeType

  RangePatternSynonym
    :: RangeType

  RangePostulate
    :: RangeType

  RangeRecord
    :: RangeType

  RangeRecordConstructor
    :: RangeType

  RangeVariable
    :: RangeType

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

-- | Information associated with an item found at a certain range.
data RangeInfo where

  RangeNamed
    :: !RangeType
    -> !QName
    -> RangeInfo

  RangeMutual
    :: RangeInfo

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

-- ## Interface

-- | Get the file path associated with the given range.
rangePath
  :: Range
  -> Maybe FilePath
rangePath :: Range -> Maybe String
rangePath (Range (S.Just AbsolutePath
p) Seq IntervalWithoutFile
_)
  = String -> Maybe String
forall a. a -> Maybe a
Just (AbsolutePath -> String
filePath AbsolutePath
p)
rangePath Range
_
  = Maybe String
forall a. Maybe a
Nothing

-- | Determine whether the first range contains the second.
rangeContains
  :: Range
  -> Range
  -> Bool
rangeContains :: Range -> Range -> Bool
rangeContains r1 :: Range
r1@(Range Maybe AbsolutePath
f1 Seq IntervalWithoutFile
_) r2 :: Range
r2@(Range Maybe AbsolutePath
f2 Seq IntervalWithoutFile
_) | Maybe AbsolutePath
f1 Maybe AbsolutePath -> Maybe AbsolutePath -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe AbsolutePath
f2
  = Maybe PositionWithoutFile
-> Maybe PositionWithoutFile
-> Maybe PositionWithoutFile
-> Maybe PositionWithoutFile
-> Bool
rangeContains' (Range -> Maybe PositionWithoutFile
forall a. Range' a -> Maybe PositionWithoutFile
rStart' Range
r1) (Range -> Maybe PositionWithoutFile
forall a. Range' a -> Maybe PositionWithoutFile
rEnd' Range
r1) (Range -> Maybe PositionWithoutFile
forall a. Range' a -> Maybe PositionWithoutFile
rStart' Range
r2) (Range -> Maybe PositionWithoutFile
forall a. Range' a -> Maybe PositionWithoutFile
rEnd' Range
r2)
rangeContains Range
_ Range
_
  = Bool
False

rangeContains'
  :: Maybe PositionWithoutFile
  -> Maybe PositionWithoutFile
  -> Maybe PositionWithoutFile
  -> Maybe PositionWithoutFile
  -> Bool
rangeContains' :: Maybe PositionWithoutFile
-> Maybe PositionWithoutFile
-> Maybe PositionWithoutFile
-> Maybe PositionWithoutFile
-> Bool
rangeContains' (Just PositionWithoutFile
s1) (Just PositionWithoutFile
e1) (Just PositionWithoutFile
s2) (Just PositionWithoutFile
e2)
  = PositionWithoutFile
s1 PositionWithoutFile -> PositionWithoutFile -> Bool
forall a. Ord a => a -> a -> Bool
<= PositionWithoutFile
s2 Bool -> Bool -> Bool
&& PositionWithoutFile
e1 PositionWithoutFile -> PositionWithoutFile -> Bool
forall a. Ord a => a -> a -> Bool
>= PositionWithoutFile
e2
rangeContains' Maybe PositionWithoutFile
_ Maybe PositionWithoutFile
_ Maybe PositionWithoutFile
_ Maybe PositionWithoutFile
_
  = Bool
False