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

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

  ( -- * Definitions

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

    -- * Interface

  , getRange
  , rangeContains

  ) where

import Agda.Unused.Types.Name
  (QName)

import Agda.Syntax.Position
  (PositionWithoutFile, Range, Range'(..), getRange, rEnd', rStart')

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

-- | Determine whether the first range contains the second.
rangeContains
  :: Range
  -> Range
  -> Bool
rangeContains :: Range -> Range -> Bool
rangeContains r1 :: Range
r1 r2 :: Range
r2
  = 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'
  :: Maybe PositionWithoutFile
  -> Maybe PositionWithoutFile
  -> Maybe PositionWithoutFile
  -> Maybe PositionWithoutFile
  -> Bool
rangeContains' :: Maybe PositionWithoutFile
-> Maybe PositionWithoutFile
-> Maybe PositionWithoutFile
-> Maybe PositionWithoutFile
-> Bool
rangeContains' (Just s1 :: PositionWithoutFile
s1) (Just e1 :: PositionWithoutFile
e1) (Just s2 :: PositionWithoutFile
s2) (Just e2 :: 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' _ _ _ _
  = Bool
False