Agda.Unused.Types.Range

Location ranges of Agda code files.

Definitions

type Range = Range' SrcFile

data Range' a

A range is a file name, plus a sequence of intervals, assumed to point to the given file. The intervals should be consecutive and separated.

Note the invariant which ranges have to satisfy: rangeInvariant.

Constructors

NoRange

Range !a (Seq IntervalWithoutFile)

Instances

Functor Range'

Defined in Agda.Syntax.Position

Methods

fmap :: (a -> b) -> Range' a -> Range' b

(<$) :: a -> Range' b -> Range' a

Foldable Range'

Defined in Agda.Syntax.Position

Methods

fold :: Monoid m => Range' m -> m

foldMap :: Monoid m => (a -> m) -> Range' a -> m

foldMap' :: Monoid m => (a -> m) -> Range' a -> m

foldr :: (a -> b -> b) -> b -> Range' a -> b

foldr' :: (a -> b -> b) -> b -> Range' a -> b

foldl :: (b -> a -> b) -> b -> Range' a -> b

foldl' :: (b -> a -> b) -> b -> Range' a -> b

foldr1 :: (a -> a -> a) -> Range' a -> a

foldl1 :: (a -> a -> a) -> Range' a -> a

toList :: Range' a -> [a]

null :: Range' a -> Bool

length :: Range' a -> Int

elem :: Eq a => a -> Range' a -> Bool

maximum :: Ord a => Range' a -> a

minimum :: Ord a => Range' a -> a

sum :: Num a => Range' a -> a

product :: Num a => Range' a -> a

Traversable Range'

Defined in Agda.Syntax.Position

Methods

traverse :: Applicative f => (a -> f b) -> Range' a -> f (Range' b)

sequenceA :: Applicative f => Range' (f a) -> f (Range' a)

mapM :: Monad m => (a -> m b) -> Range' a -> m (Range' b)

sequence :: Monad m => Range' (m a) -> m (Range' a)

FreshName Range

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadFresh NameId m => Range -> m Name

HasRange Range

Defined in Agda.Syntax.Position

Methods

getRange :: Range -> Range

SetRange Range

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> Range -> Range

KillRange Range

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Range

LensClosure Range MetaVariable

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' (Closure Range) MetaVariable

LensClosure Range MetaInfo

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' (Closure Range) MetaInfo

Eq a => Eq (Range' a)

Defined in Agda.Syntax.Position

Methods

(==) :: Range' a -> Range' a -> Bool

(/=) :: Range' a -> Range' a -> Bool

Data a => Data (Range' a)

Defined in Agda.Syntax.Position

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Range' a -> c (Range' a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Range' a)

toConstr :: Range' a -> Constr

dataTypeOf :: Range' a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Range' a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Range' a))

gmapT :: (forall b. Data b => b -> b) -> Range' a -> Range' a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Range' a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Range' a -> r

gmapQ :: (forall d. Data d => d -> u) -> Range' a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Range' a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Range' a -> m (Range' a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Range' a -> m (Range' a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Range' a -> m (Range' a)

Ord a => Ord (Range' a)

Defined in Agda.Syntax.Position

Methods

compare :: Range' a -> Range' a -> Ordering

(<) :: Range' a -> Range' a -> Bool

(<=) :: Range' a -> Range' a -> Bool

(>) :: Range' a -> Range' a -> Bool

(>=) :: Range' a -> Range' a -> Bool

max :: Range' a -> Range' a -> Range' a

min :: Range' a -> Range' a -> Range' a

Show a => Show (Range' (Maybe a))

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> Range' (Maybe a) -> ShowS

show :: Range' (Maybe a) -> String

showList :: [Range' (Maybe a)] -> ShowS

Show a => Show (Range' (Maybe a))

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> Range' (Maybe a) -> ShowS

show :: Range' (Maybe a) -> String

showList :: [Range' (Maybe a)] -> ShowS

Generic (Range' a)

Defined in Agda.Syntax.Position

Associated Types

type Rep (Range' a) :: Type -> Type

Methods

from :: Range' a -> Rep (Range' a) x

to :: Rep (Range' a) x -> Range' a

Pretty a => Pretty (Range' (Maybe a))

Defined in Agda.Syntax.Position

Methods

pretty :: Range' (Maybe a) -> Doc

prettyPrec :: Int -> Range' (Maybe a) -> Doc

prettyList :: [Range' (Maybe a)] -> Doc

Null (Range' a)

Defined in Agda.Syntax.Position

Methods

empty :: Range' a

null :: Range' a -> Bool

FreshName (Range, String)

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadFresh NameId m => (Range, String) -> m Name

type Rep (Range' a)

Defined in Agda.Syntax.Position

type Rep (Range' a) = D1 ('MetaData "Range'" "Agda.Syntax.Position" "Agda-2.6.1.3-2WluKmOFu84Cr2Fuyr5biZ" 'False) (C1 ('MetaCons "NoRange" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Range" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Seq IntervalWithoutFile))))

data RangeType where

The type of item found at a named range.

Constructors

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

Instances

Eq RangeType

Defined in Agda.Unused.Types.Range

Methods

(==) :: RangeType -> RangeType -> Bool

(/=) :: RangeType -> RangeType -> Bool

Ord RangeType

Defined in Agda.Unused.Types.Range

Methods

compare :: RangeType -> RangeType -> Ordering

(<) :: RangeType -> RangeType -> Bool

(<=) :: RangeType -> RangeType -> Bool

(>) :: RangeType -> RangeType -> Bool

(>=) :: RangeType -> RangeType -> Bool

max :: RangeType -> RangeType -> RangeType

min :: RangeType -> RangeType -> RangeType

Show RangeType

Defined in Agda.Unused.Types.Range

Methods

showsPrec :: Int -> RangeType -> ShowS

show :: RangeType -> String

showList :: [RangeType] -> ShowS

data RangeInfo where

Information associated with an item found at a certain range.

Constructors

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

RangeMutual :: RangeInfo

Instances

Eq RangeInfo

Defined in Agda.Unused.Types.Range

Methods

(==) :: RangeInfo -> RangeInfo -> Bool

(/=) :: RangeInfo -> RangeInfo -> Bool

Ord RangeInfo

Defined in Agda.Unused.Types.Range

Methods

compare :: RangeInfo -> RangeInfo -> Ordering

(<) :: RangeInfo -> RangeInfo -> Bool

(<=) :: RangeInfo -> RangeInfo -> Bool

(>) :: RangeInfo -> RangeInfo -> Bool

(>=) :: RangeInfo -> RangeInfo -> Bool

max :: RangeInfo -> RangeInfo -> RangeInfo

min :: RangeInfo -> RangeInfo -> RangeInfo

Show RangeInfo

Defined in Agda.Unused.Types.Range

Methods

showsPrec :: Int -> RangeInfo -> ShowS

show :: RangeInfo -> String

showList :: [RangeInfo] -> ShowS

Interface

getRange :: HasRange t => t -> Range

rangePath :: Range -> Maybe FilePath

Get the file path associated with the given range.

rangeContains :: Range -> Range -> Bool

Determine whether the first range contains the second.