Safe Haskell	None
Language	Haskell2010

Agda.Unused.Types.Range

Contents

Definitions
Interface

Description

Location ranges of Agda code files.

Synopsis

type Range = Range' SrcFile
data Range' a
- = NoRange
- | Range !a (Seq IntervalWithoutFile)
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
data RangeInfo where
- RangeNamed :: !RangeType -> !QName -> RangeInfo
- RangeMutual :: RangeInfo
getRange :: HasRange t => t -> Range
rangePath :: Range -> Maybe FilePath
rangeContains :: Range -> Range -> Bool

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

Instances details

Functor Range'
Instance details Defined in Agda.Syntax.Position Methods fmap :: (a -> b) -> Range' a -> Range' b # (<$) :: a -> Range' b -> Range' a #
Foldable Range'
Instance details 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'
Instance details 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
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => Range -> m Name #
HasRange Range
Instance details Defined in Agda.Syntax.Position Methods getRange :: Range -> Range #
SetRange Range
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> Range -> Range #
KillRange Range
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Range #
LensClosure Range MetaVariable
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lensClosure :: Lens' (Closure Range) MetaVariable #
LensClosure Range MetaInfo
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lensClosure :: Lens' (Closure Range) MetaInfo #
Eq a => Eq (Range' a)
Instance details Defined in Agda.Syntax.Position Methods (==) :: Range' a -> Range' a -> Bool # (/=) :: Range' a -> Range' a -> Bool #
Data a => Data (Range' a)
Instance details 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)
Instance details 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))
Instance details 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))
Instance details 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)
Instance details 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))
Instance details 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)
Instance details Defined in Agda.Syntax.Position Methods empty :: Range' a # null :: Range' a -> Bool #
FreshName (Range, String)
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => (Range, String) -> m Name #
type Rep (Range' a)
Instance details 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 Source #

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

Instances details

Eq RangeType Source #
Instance details Defined in Agda.Unused.Types.Range Methods (==) :: RangeType -> RangeType -> Bool # (/=) :: RangeType -> RangeType -> Bool #
Ord RangeType Source #
Instance details 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 Source #
Instance details Defined in Agda.Unused.Types.Range Methods showsPrec :: Int -> RangeType -> ShowS # show :: RangeType -> String # showList :: [RangeType] -> ShowS #

data RangeInfo where Source #

Information associated with an item found at a certain range.

Constructors

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

Instances

Instances details

Eq RangeInfo Source #
Instance details Defined in Agda.Unused.Types.Range Methods (==) :: RangeInfo -> RangeInfo -> Bool # (/=) :: RangeInfo -> RangeInfo -> Bool #
Ord RangeInfo Source #
Instance details 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 Source #
Instance details 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 Source #

Get the file path associated with the given range.

rangeContains :: Range -> Range -> Bool Source #

Determine whether the first range contains the second.