module Agda.Unused.Types.Range
(
RangeType(..)
, RangeInfo(..)
, rangePath
, rangeContains
) where
import Agda.Unused.Types.Name
(QName)
import Agda.Syntax.Position
(PositionWithoutFile, Range, Range'(..), rEnd', rStart')
import Agda.Utils.FileName
(filePath)
import qualified Agda.Utils.Maybe.Strict
as S
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
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
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
Ord, Int -> RangeType -> ShowS
[RangeType] -> ShowS
RangeType -> String
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)
data RangeInfo where
RangeNamed
:: !RangeType
-> !QName
-> RangeInfo
RangeMutual
:: RangeInfo
deriving (RangeInfo -> RangeInfo -> Bool
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
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
Ord, Int -> RangeInfo -> ShowS
[RangeInfo] -> ShowS
RangeInfo -> String
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)
rangePath
:: Range
-> Maybe FilePath
rangePath :: Range -> Maybe String
rangePath (Range (S.Just AbsolutePath
p) Seq IntervalWithoutFile
_)
= forall a. a -> Maybe a
Just (AbsolutePath -> String
filePath AbsolutePath
p)
rangePath Range
_
= forall a. Maybe a
Nothing
rangeContains
:: Range
-> Range
-> Bool
rangeContains :: Range -> Range -> Bool
rangeContains r1 :: Range
r1@(Range SrcFile
f1 Seq IntervalWithoutFile
_) r2 :: Range
r2@(Range SrcFile
f2 Seq IntervalWithoutFile
_) | SrcFile
f1 forall a. Eq a => a -> a -> Bool
== SrcFile
f2
= Maybe PositionWithoutFile
-> Maybe PositionWithoutFile
-> Maybe PositionWithoutFile
-> Maybe PositionWithoutFile
-> Bool
rangeContains' (forall a. Range' a -> Maybe PositionWithoutFile
rStart' Range
r1) (forall a. Range' a -> Maybe PositionWithoutFile
rEnd' Range
r1) (forall a. Range' a -> Maybe PositionWithoutFile
rStart' Range
r2) (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 forall a. Ord a => a -> a -> Bool
<= PositionWithoutFile
s2 Bool -> Bool -> Bool
&& PositionWithoutFile
e1 forall a. Ord a => a -> a -> Bool
>= PositionWithoutFile
e2
rangeContains' Maybe PositionWithoutFile
_ Maybe PositionWithoutFile
_ Maybe PositionWithoutFile
_ Maybe PositionWithoutFile
_
= Bool
False