Agda-2.8.0: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Position

Description

Position information for syntax. Crucial for giving good error messages.

Synopsis

Positions

type Position = Position' SrcFile Source #

type PositionWithoutFile = Position' () Source #

data Position' a Source #

Represents a point in the input.

If two positions have the same srcFile and posPos components, then the final two components should be the same as well, but since this can be hard to enforce the program should not rely too much on the last two components; they are mainly there to improve error messages for the user.

Note the invariant which positions have to satisfy: positionInvariant.

Constructors

Pn 

Fields

Instances

Instances details
Pretty PositionWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: PositionWithoutFile -> Doc Source #

prettyPrec :: Int -> PositionWithoutFile -> Doc Source #

prettyList :: [PositionWithoutFile] -> Doc Source #

Foldable Position' Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

fold :: Monoid m => Position' m -> m #

foldMap :: Monoid m => (a -> m) -> Position' a -> m #

foldMap' :: Monoid m => (a -> m) -> Position' a -> m #

foldr :: (a -> b -> b) -> b -> Position' a -> b #

foldr' :: (a -> b -> b) -> b -> Position' a -> b #

foldl :: (b -> a -> b) -> b -> Position' a -> b #

foldl' :: (b -> a -> b) -> b -> Position' a -> b #

foldr1 :: (a -> a -> a) -> Position' a -> a #

foldl1 :: (a -> a -> a) -> Position' a -> a #

toList :: Position' a -> [a] #

null :: Position' a -> Bool #

length :: Position' a -> Int #

elem :: Eq a => a -> Position' a -> Bool #

maximum :: Ord a => Position' a -> a #

minimum :: Ord a => Position' a -> a #

sum :: Num a => Position' a -> a #

product :: Num a => Position' a -> a #

Traversable Position' Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

sequenceA :: Applicative f => Position' (f a) -> f (Position' a) #

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

sequence :: Monad m => Position' (m a) -> m (Position' a) #

Functor Position' Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

fmap :: (a -> b) -> Position' a -> Position' b #

(<$) :: a -> Position' b -> Position' a #

NFData Position Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

rnf :: Position -> () #

NFData PositionWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

rnf :: PositionWithoutFile -> () #

EncodeTCM (Position' ()) Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Position' () -> TCM Value Source #

Pretty a => Pretty (Position' (Maybe a)) Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Position' (Maybe a) -> Doc Source #

prettyPrec :: Int -> Position' (Maybe a) -> Doc Source #

prettyList :: [Position' (Maybe a)] -> Doc Source #

EmbPrj a => EmbPrj (Position' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Position' a -> S Word32 Source #

icod_ :: Position' a -> S Word32 Source #

value :: Word32 -> R (Position' a) Source #

ToJSON (Position' ()) Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: Position' () -> Value #

toEncoding :: Position' () -> Encoding #

toJSONList :: [Position' ()] -> Value #

toEncodingList :: [Position' ()] -> Encoding #

omitField :: Position' () -> Bool #

Generic (Position' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Associated Types

type Rep (Position' a) 
Instance details

Defined in Agda.Syntax.Position

type Rep (Position' a) = D1 ('MetaData "Position'" "Agda.Syntax.Position" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "Pn" 'PrefixI 'True) ((S1 ('MetaSel ('Just "srcFile") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a) :*: S1 ('MetaSel ('Just "posPos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Word32)) :*: (S1 ('MetaSel ('Just "posLine") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Word32) :*: S1 ('MetaSel ('Just "posCol") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Word32))))

Methods

from :: Position' a -> Rep (Position' a) x #

to :: Rep (Position' a) x -> Position' a #

Read a => Read (Position' a) Source # 
Instance details

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS (Position' a) #

readList :: ReadS [Position' a] #

readPrec :: ReadPrec (Position' a) #

readListPrec :: ReadPrec [Position' a] #

Show a => Show (Position' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> Position' a -> ShowS #

show :: Position' a -> String #

showList :: [Position' a] -> ShowS #

Eq a => Eq (Position' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

(==) :: Position' a -> Position' a -> Bool #

(/=) :: Position' a -> Position' a -> Bool #

Ord a => Ord (Position' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

compare :: Position' a -> Position' a -> Ordering #

(<) :: Position' a -> Position' a -> Bool #

(<=) :: Position' a -> Position' a -> Bool #

(>) :: Position' a -> Position' a -> Bool #

(>=) :: Position' a -> Position' a -> Bool #

max :: Position' a -> Position' a -> Position' a #

min :: Position' a -> Position' a -> Position' a #

type Rep (Position' a) Source # 
Instance details

Defined in Agda.Syntax.Position

type Rep (Position' a) = D1 ('MetaData "Position'" "Agda.Syntax.Position" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "Pn" 'PrefixI 'True) ((S1 ('MetaSel ('Just "srcFile") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a) :*: S1 ('MetaSel ('Just "posPos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Word32)) :*: (S1 ('MetaSel ('Just "posLine") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Word32) :*: S1 ('MetaSel ('Just "posCol") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Word32))))

type SrcFile = Maybe RangeFile Source #

data RangeFile Source #

File information used in the Position, Interval and Range types.

Constructors

RangeFile 

Fields

  • rangeFilePath :: !AbsolutePath

    The file's path.

  • rangeFileName :: !(Maybe (TopLevelModuleName' Range))

    The file's top-level module name (if applicable).

    This field is optional, but some things may break if the field is not instantiated with an actual top-level module name. For instance, the Eq and Ord instances only make use of this field.

    The field uses Maybe rather than Maybe because it should be possible to instantiate it with something that is not yet defined (see parseSource).

    This '(TopLevelModuleName' Range)' should not contain a range.

Instances

Instances details
EncodeTCM Range Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Range -> TCM Value Source #

Pretty RangeFile Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: RangeFile -> Doc Source #

prettyPrec :: Int -> RangeFile -> Doc Source #

prettyList :: [RangeFile] -> Doc Source #

Pretty TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

pretty :: TopLevelModuleName -> Doc Source #

prettyPrec :: Int -> TopLevelModuleName -> Doc Source #

prettyList :: [TopLevelModuleName] -> Doc Source #

HasRange Interval Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Interval -> Range Source #

HasRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Range -> Range Source #

KillRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Range Source #

SetRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> Range -> Range Source #

FreshName Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

PrettyTCM Range Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Range -> m Doc Source #

PrettyTCM TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => TopLevelModuleName -> m Doc Source #

EmbPrj Range Source #

Ranges are always deserialised as noRange.

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Range -> S Word32 Source #

icod_ :: Range -> S Word32 Source #

value :: Word32 -> R Range Source #

EmbPrj RangeFile Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: RangeFile -> S Word32 Source #

icod_ :: RangeFile -> S Word32 Source #

value :: Word32 -> R RangeFile Source #

EmbPrj TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: TopLevelModuleName -> S Word32 Source #

icod_ :: TopLevelModuleName -> S Word32 Source #

value :: Word32 -> R TopLevelModuleName Source #

Subst Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Range 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg Range = Term

Methods

applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source #

Sized TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

size :: TopLevelModuleName -> Int Source #

natSize :: TopLevelModuleName -> Peano Source #

ToJSON Range Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: Range -> Value #

toEncoding :: Range -> Encoding #

toJSONList :: [Range] -> Value #

toEncodingList :: [Range] -> Encoding #

omitField :: Range -> Bool #

Generic RangeFile Source # 
Instance details

Defined in Agda.Syntax.Position

Associated Types

type Rep RangeFile 
Instance details

Defined in Agda.Syntax.Position

type Rep RangeFile = D1 ('MetaData "RangeFile" "Agda.Syntax.Position" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "RangeFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "rangeFilePath") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 AbsolutePath) :*: S1 ('MetaSel ('Just "rangeFileName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (TopLevelModuleName' Range)))))

Methods

from :: RangeFile -> Rep RangeFile x #

to :: Rep RangeFile x -> RangeFile #

Read RangeFile Source #

This instance fills in the TopLevelModuleNames using Nothing. Note that these occurrences of Nothing are "overwritten" by parseIOTCM.

Instance details

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS RangeFile #

readList :: ReadS [RangeFile] #

readPrec :: ReadPrec RangeFile #

readListPrec :: ReadPrec [RangeFile] #

Show RangeFile Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> RangeFile -> ShowS #

show :: RangeFile -> String #

showList :: [RangeFile] -> ShowS #

NFData Interval Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

rnf :: Interval -> () #

NFData Position Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

rnf :: Position -> () #

NFData RangeFile Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

rnf :: RangeFile -> () #

Eq RangeFile Source #

Only the rangeFileName component is compared.

Instance details

Defined in Agda.Syntax.Position

Methods

(==) :: RangeFile -> RangeFile -> Bool #

(/=) :: RangeFile -> RangeFile -> Bool #

Ord RangeFile Source #

Only the rangeFileName component is compared.

Instance details

Defined in Agda.Syntax.Position

Methods

compare :: RangeFile -> RangeFile -> Ordering #

(<) :: RangeFile -> RangeFile -> Bool #

(<=) :: RangeFile -> RangeFile -> Bool #

(>) :: RangeFile -> RangeFile -> Bool #

(>=) :: RangeFile -> RangeFile -> Bool #

max :: RangeFile -> RangeFile -> RangeFile #

min :: RangeFile -> RangeFile -> RangeFile #

LensClosure MetaInfo Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' MetaInfo (Closure Range) Source #

LensClosure MetaVariable Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' MetaVariable (Closure Range) Source #

HasRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: TopLevelModuleName' Range -> Range Source #

KillRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (TopLevelModuleName' Range) Source #

SetRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> TopLevelModuleName' Range -> TopLevelModuleName' Range Source #

FreshName (Range, String) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

type SubstArg Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg Range = Term
type Rep RangeFile Source # 
Instance details

Defined in Agda.Syntax.Position

type Rep RangeFile = D1 ('MetaData "RangeFile" "Agda.Syntax.Position" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "RangeFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "rangeFilePath") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 AbsolutePath) :*: S1 ('MetaSel ('Just "rangeFileName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (TopLevelModuleName' Range)))))

mkRangeFile :: AbsolutePath -> Maybe (TopLevelModuleName' Range) -> RangeFile Source #

A smart constructor for RangeFile.

positionInvariant :: Position' a -> Bool Source #

startPos :: Maybe RangeFile -> Position Source #

The first position in a file: position 1, line 1, column 1.

startPos' :: a -> Position' a Source #

The first position in a file: position 1, line 1, column 1.

movePos :: Position' a -> Char -> Position' a Source #

Advance the position by one character. A newline character ('n') moves the position to the first character in the next line. Any other character moves the position to the next column.

movePosByString :: Foldable t => Position' a -> t Char -> Position' a Source #

Advance the position by a string.

movePosByString = foldl' movePos

backupPos :: Position' a -> Position' a Source #

Backup the position by one character.

Precondition: The character must not be 'n'.

Intervals

type Interval = Interval' SrcFile Source #

type IntervalWithoutFile = Interval' () Source #

data Interval' a Source #

An interval. The iEnd position is not included in the interval.

Note the invariant which intervals have to satisfy: intervalInvariant.

Constructors

Interval a !PositionWithoutFile !PositionWithoutFile 

Instances

Instances details
Pretty IntervalWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: IntervalWithoutFile -> Doc Source #

prettyPrec :: Int -> IntervalWithoutFile -> Doc Source #

prettyList :: [IntervalWithoutFile] -> Doc Source #

HasRange Interval Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Interval -> Range Source #

HasRangeWithoutFile IntervalWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: IntervalWithoutFile -> RangeWithoutFile Source #

Foldable Interval' Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

fold :: Monoid m => Interval' m -> m #

foldMap :: Monoid m => (a -> m) -> Interval' a -> m #

foldMap' :: Monoid m => (a -> m) -> Interval' a -> m #

foldr :: (a -> b -> b) -> b -> Interval' a -> b #

foldr' :: (a -> b -> b) -> b -> Interval' a -> b #

foldl :: (b -> a -> b) -> b -> Interval' a -> b #

foldl' :: (b -> a -> b) -> b -> Interval' a -> b #

foldr1 :: (a -> a -> a) -> Interval' a -> a #

foldl1 :: (a -> a -> a) -> Interval' a -> a #

toList :: Interval' a -> [a] #

null :: Interval' a -> Bool #

length :: Interval' a -> Int #

elem :: Eq a => a -> Interval' a -> Bool #

maximum :: Ord a => Interval' a -> a #

minimum :: Ord a => Interval' a -> a #

sum :: Num a => Interval' a -> a #

product :: Num a => Interval' a -> a #

Traversable Interval' Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

sequenceA :: Applicative f => Interval' (f a) -> f (Interval' a) #

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

sequence :: Monad m => Interval' (m a) -> m (Interval' a) #

Functor Interval' Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

fmap :: (a -> b) -> Interval' a -> Interval' b #

(<$) :: a -> Interval' b -> Interval' a #

NFData Interval Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

rnf :: Interval -> () #

NFData IntervalWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

rnf :: IntervalWithoutFile -> () #

Pretty a => Pretty (Interval' (Maybe a)) Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Interval' (Maybe a) -> Doc Source #

prettyPrec :: Int -> Interval' (Maybe a) -> Doc Source #

prettyList :: [Interval' (Maybe a)] -> Doc Source #

EmbPrj a => EmbPrj (Interval' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Interval' a -> S Word32 Source #

icod_ :: Interval' a -> S Word32 Source #

value :: Word32 -> R (Interval' a) Source #

Generic (Interval' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Associated Types

type Rep (Interval' a) 
Instance details

Defined in Agda.Syntax.Position

type Rep (Interval' a) = D1 ('MetaData "Interval'" "Agda.Syntax.Position" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "Interval" 'PrefixI 'True) (S1 ('MetaSel ('Just "getIntervalFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Just "iStart'") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PositionWithoutFile) :*: S1 ('MetaSel ('Just "iEnd'") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PositionWithoutFile))))

Methods

from :: Interval' a -> Rep (Interval' a) x #

to :: Rep (Interval' a) x -> Interval' a #

Read a => Read (Interval' a) Source # 
Instance details

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS (Interval' a) #

readList :: ReadS [Interval' a] #

readPrec :: ReadPrec (Interval' a) #

readListPrec :: ReadPrec [Interval' a] #

Show a => Show (Interval' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> Interval' a -> ShowS #

show :: Interval' a -> String #

showList :: [Interval' a] -> ShowS #

Eq a => Eq (Interval' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

(==) :: Interval' a -> Interval' a -> Bool #

(/=) :: Interval' a -> Interval' a -> Bool #

Ord a => Ord (Interval' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

compare :: Interval' a -> Interval' a -> Ordering #

(<) :: Interval' a -> Interval' a -> Bool #

(<=) :: Interval' a -> Interval' a -> Bool #

(>) :: Interval' a -> Interval' a -> Bool #

(>=) :: Interval' a -> Interval' a -> Bool #

max :: Interval' a -> Interval' a -> Interval' a #

min :: Interval' a -> Interval' a -> Interval' a #

type Rep (Interval' a) Source # 
Instance details

Defined in Agda.Syntax.Position

type Rep (Interval' a) = D1 ('MetaData "Interval'" "Agda.Syntax.Position" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "Interval" 'PrefixI 'True) (S1 ('MetaSel ('Just "getIntervalFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Just "iStart'") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PositionWithoutFile) :*: S1 ('MetaSel ('Just "iEnd'") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PositionWithoutFile))))

intervalInvariant :: Ord a => Interval' a -> Bool Source #

iStart :: Interval' a -> Position' a Source #

iEnd :: Interval' a -> Position' a Source #

posToInterval :: a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a Source #

Converts a file name and two positions to an interval. Sort the positions ascendingly.

getIntervalFile :: Interval' a -> a Source #

iLength :: Interval' a -> Word32 Source #

The length of an interval.

fuseIntervals :: IntervalWithoutFile -> IntervalWithoutFile -> IntervalWithoutFile Source #

Finds the least interval which covers the arguments.

Ranges

type Range = Range' SrcFile Source #

type RangeWithoutFile = Range' () Source #

data Range' a Source #

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
EncodeTCM Range Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Range -> TCM Value Source #

Pretty TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

pretty :: TopLevelModuleName -> Doc Source #

prettyPrec :: Int -> TopLevelModuleName -> Doc Source #

prettyList :: [TopLevelModuleName] -> Doc Source #

HasRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Range -> Range Source #

HasRangeWithoutFile RangeWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: RangeWithoutFile -> RangeWithoutFile Source #

KillRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Range Source #

SetRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> Range -> Range Source #

FreshName Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

PrettyTCM Range Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Range -> m Doc Source #

PrettyTCM TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => TopLevelModuleName -> m Doc Source #

EmbPrj Range Source #

Ranges are always deserialised as noRange.

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Range -> S Word32 Source #

icod_ :: Range -> S Word32 Source #

value :: Word32 -> R Range Source #

EmbPrj TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: TopLevelModuleName -> S Word32 Source #

icod_ :: TopLevelModuleName -> S Word32 Source #

value :: Word32 -> R TopLevelModuleName Source #

Subst Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Range 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg Range = Term

Methods

applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source #

Sized TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

size :: TopLevelModuleName -> Int Source #

natSize :: TopLevelModuleName -> Peano Source #

ToJSON Range Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: Range -> Value #

toEncoding :: Range -> Encoding #

toJSONList :: [Range] -> Value #

toEncodingList :: [Range] -> Encoding #

omitField :: Range -> Bool #

Foldable Range' Source # 
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' Source # 
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) #

Functor Range' Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

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

LensClosure MetaInfo Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' MetaInfo (Closure Range) Source #

LensClosure MetaVariable Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' MetaVariable (Closure Range) Source #

Pretty a => Pretty (Range' (Maybe a)) Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

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

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

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

HasRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: TopLevelModuleName' Range -> Range Source #

KillRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (TopLevelModuleName' Range) Source #

SetRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> TopLevelModuleName' Range -> TopLevelModuleName' Range Source #

Null (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

empty :: Range' a Source #

null :: Range' a -> Bool Source #

Eq a => Monoid (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

mempty :: Range' a #

mappend :: Range' a -> Range' a -> Range' a #

mconcat :: [Range' a] -> Range' a #

Eq a => Semigroup (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

sconcat :: NonEmpty (Range' a) -> Range' a #

stimes :: Integral b => b -> Range' a -> Range' a #

Generic (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Associated Types

type Rep (Range' a) 
Instance details

Defined in Agda.Syntax.Position

type Rep (Range' a) = D1 ('MetaData "Range'" "Agda.Syntax.Position" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" '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))))

Methods

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

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

Read a => Read (Range' a) Source #

Note that the grammar implemented by this instance does not necessarily match the current representation of ranges.

Instance details

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS (Range' a) #

readList :: ReadS [Range' a] #

readPrec :: ReadPrec (Range' a) #

readListPrec :: ReadPrec [Range' a] #

Show a => Show (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> Range' a -> ShowS #

show :: Range' a -> String #

showList :: [Range' a] -> ShowS #

NFData a => NFData (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

rnf :: Range' a -> () #

Eq a => Eq (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

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

Ord a => Ord (Range' a) Source # 
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 #

FreshName (Range, String) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

type SubstArg Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg Range = Term
type Rep (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

type Rep (Range' a) = D1 ('MetaData "Range'" "Agda.Syntax.Position" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" '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))))

rangeInvariant :: Ord a => Range' a -> Bool Source #

Range invariant.

consecutiveAndSeparated :: Ord a => [Interval' a] -> Bool Source #

Are the intervals consecutive and separated, do they all point to the same file, and do they satisfy the interval invariant?

intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a Source #

Turns a file name plus a list of intervals into a range.

Precondition: consecutiveAndSeparated.

intervalToRange :: a -> IntervalWithoutFile -> Range' a Source #

Converts a file name and an interval to a range.

rangeFromAbsolutePath :: AbsolutePath -> Range Source #

Range pointing to the first position in the given file.

rangeIntervals :: Range' a -> [IntervalWithoutFile] Source #

The intervals that make up the range. The intervals are consecutive and separated (consecutiveAndSeparated).

rangeFile :: Range -> SrcFile Source #

The file the range is pointing to.

rangeModule' :: Range -> Maybe (Maybe (TopLevelModuleName' Range)) Source #

The range's top-level module name, if any.

If there is no range, then Nothing is returned. If there is a range without a module name, then Just Nothing is returned.

rangeModule :: Range -> Maybe (TopLevelModuleName' Range) Source #

The range's top-level module name, if any.

rightMargin :: Range -> Range Source #

Conflate a range to its right margin.

noRange :: Range' a Source #

Ranges between two unknown positions

posToRange :: Position' a -> Position' a -> Range' a Source #

Converts two positions to a range.

Precondition: The positions have to point to the same file.

posToRange' :: a -> PositionWithoutFile -> PositionWithoutFile -> Range' a Source #

Converts a file name and two positions to a range.

rStart :: Range' a -> Maybe (Position' a) Source #

The initial position in the range, if any.

rStart' :: Range' a -> Maybe PositionWithoutFile Source #

The initial position in the range, if any.

rEnd :: Range' a -> Maybe (Position' a) Source #

The position after the final position in the range, if any.

rEnd' :: Range' a -> Maybe PositionWithoutFile Source #

The position after the final position in the range, if any.

rangeToInterval :: Range' a -> Maybe IntervalWithoutFile Source #

Converts a range to an interval, if possible. Note that the information about the source file is lost.

rangeToIntervalWithFile :: Range' a -> Maybe (Interval' a) Source #

Converts a range to an interval, if possible.

continuous :: Range' a -> Range' a Source #

Returns the shortest continuous range containing the given one.

continuousPerLine :: Ord a => Range' a -> Range' a Source #

Removes gaps between intervals on the same line.

newtype PrintRange a Source #

Wrapper to indicate that range should be printed.

Constructors

PrintRange a 

Instances

Instances details
(Pretty a, HasRange a) => Pretty (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: PrintRange a -> Doc Source #

prettyPrec :: Int -> PrintRange a -> Doc Source #

prettyList :: [PrintRange a] -> Doc Source #

HasRange a => HasRange (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: PrintRange a -> Range Source #

KillRange a => KillRange (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (PrintRange a) Source #

SetRange a => SetRange (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> PrintRange a -> PrintRange a Source #

Eq a => Eq (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

(==) :: PrintRange a -> PrintRange a -> Bool #

(/=) :: PrintRange a -> PrintRange a -> Bool #

Ord a => Ord (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

compare :: PrintRange a -> PrintRange a -> Ordering #

(<) :: PrintRange a -> PrintRange a -> Bool #

(<=) :: PrintRange a -> PrintRange a -> Bool #

(>) :: PrintRange a -> PrintRange a -> Bool #

(>=) :: PrintRange a -> PrintRange a -> Bool #

max :: PrintRange a -> PrintRange a -> PrintRange a #

min :: PrintRange a -> PrintRange a -> PrintRange a #

class HasRange a where Source #

Things that have a range are instances of this class.

Minimal complete definition

Nothing

Methods

getRange :: a -> Range Source #

default getRange :: forall (t :: Type -> Type) b. (Foldable t, HasRange b, t b ~ a) => a -> Range Source #

Instances

Instances details
HasRange HaskellPragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pragmas

Methods

getRange :: HaskellPragma -> Range Source #

HasRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: BindName -> Range Source #

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Declaration -> Range Source #

HasRange Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Expr -> Range Source #

HasRange LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHS -> Range Source #

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LamBinding -> Range Source #

HasRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LetBinding -> Range Source #

HasRange RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: RHS -> Range Source #

HasRange SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: SpineLHS -> Range Source #

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: TypedBinding -> Range Source #

HasRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: WhereDeclarations -> Range Source #

HasRange AmbiguousQName Source #

The range of an AmbiguousQName is the range of any of its disambiguations (they are the same concrete name).

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: AmbiguousQName -> Range Source #

HasRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: ModuleName -> Range Source #

HasRange Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: Name -> Range Source #

HasRange QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: QName -> Range Source #

HasRange Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Access -> Range Source #

HasRange Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Annotation -> Range Source #

HasRange ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: ArgInfo -> Range Source #

HasRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Cohesion -> Range Source #

HasRange Erased Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Erased -> Range Source #

HasRange Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Fixity -> Range Source #

HasRange Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Hiding -> Range Source #

HasRange IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: IsInstance -> Range Source #

HasRange IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: IsMacro -> Range Source #

HasRange Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Modality -> Range Source #

HasRange NotationPart Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: NotationPart -> Range Source #

HasRange Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Origin -> Range Source #

HasRange OriginIrrelevant Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: OriginIrrelevant -> Range Source #

HasRange OriginRelevant Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: OriginRelevant -> Range Source #

HasRange OriginShapeIrrelevant Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: OriginShapeIrrelevant -> Range Source #

HasRange PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: PatternOrCopattern -> Range Source #

HasRange PolarityModality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: PolarityModality -> Range Source #

HasRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Q0Origin -> Range Source #

HasRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Q1Origin -> Range Source #

HasRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Quantity -> Range Source #

HasRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: QωOrigin -> Range Source #

HasRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Relevance -> Range Source #

HasRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Induction -> Range Source #

HasRange KwRange Source # 
Instance details

Defined in Agda.Syntax.Common.KeywordRange

Methods

getRange :: KwRange -> Range Source #

HasRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: AsName -> Range Source #

HasRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: Binder -> Range Source #

HasRange BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: BoundName -> Range Source #

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: Declaration -> Range Source #

HasRange DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: DoStmt -> Range Source #

HasRange Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: Expr -> Range Source #

HasRange LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: LHS -> Range Source #

HasRange LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: LHSCore -> Range Source #

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamBinding -> Range Source #

HasRange LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamClause -> Range Source #

HasRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: ModuleApplication -> Range Source #

HasRange ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: ModuleAssignment -> Range Source #

HasRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: Pattern -> Range Source #

HasRange Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: Pragma -> Range Source #

HasRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: RHS -> Range Source #

HasRange RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: RecordDirective -> Range Source #

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: TypedBinding -> Range Source #

HasRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: WhereClause -> Range Source #

HasRange Attr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

Methods

getRange :: Attr -> Range Source #

HasRange Attribute Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

Methods

getRange :: Attribute -> Range Source #

HasRange DeclarationException Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationException -> Range Source #

HasRange DeclarationException' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationException' -> Range Source #

HasRange DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationWarning -> Range Source #

HasRange DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationWarning' -> Range Source #

HasRange NiceDeclaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

getRange :: NiceDeclaration -> Range Source #

HasRange Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: Name -> Range Source #

HasRange QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: QName -> Range Source #

HasRange AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: AppInfo -> Range Source #

HasRange ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: ConPatInfo -> Range Source #

HasRange DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: DeclInfo -> Range Source #

HasRange ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: ExprInfo -> Range Source #

HasRange LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: LHSInfo -> Range Source #

HasRange LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: LetInfo -> Range Source #

HasRange MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: MetaInfo -> Range Source #

HasRange ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: ModuleInfo -> Range Source #

HasRange MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: MutualInfo -> Range Source #

HasRange PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: PatInfo -> Range Source #

HasRange Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getRange :: Clause -> Range Source #

HasRange ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getRange :: ConHead -> Range Source #

HasRange ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Methods

getRange :: ParseError -> Range Source #

HasRange ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Methods

getRange :: ParseWarning -> Range Source #

HasRange Token Source # 
Instance details

Defined in Agda.Syntax.Parser.Tokens

Methods

getRange :: Token -> Range Source #

HasRange Interval Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Interval -> Range Source #

HasRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Range -> Range Source #

HasRange AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

getRange :: AbstractName -> Range Source #

HasRange RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

getRange :: RawTopLevelModuleName -> Range Source #

HasRange Call Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Call -> Range Source #

HasRange CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: CallInfo -> Range Source #

HasRange CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: CompilerPragma -> Range Source #

HasRange Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Constraint -> Range Source #

HasRange MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: MetaInfo -> Range Source #

HasRange MetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: MetaVariable -> Range Source #

HasRange ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: ProblemConstraint -> Range Source #

HasRange TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: TCErr -> Range Source #

HasRange TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: TCWarning -> Range Source #

HasRange Item Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

getRange :: Item -> Range Source #

HasRange () Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: () -> Range Source #

HasRange Bool Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Bool -> Range Source #

HasRange a => HasRange (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Binder' a -> Range Source #

HasRange a => HasRange (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Clause' a -> Range Source #

HasRange (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHSCore' e -> Range Source #

HasRange (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Pattern' e -> Range Source #

HasRange a => HasRange (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Arg a -> Range Source #

HasRange a => HasRange (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: HasEta' a -> Range Source #

HasRange a => HasRange (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: MaybePlaceholder a -> Range Source #

HasRange (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Ranged a -> Range Source #

HasRange a => HasRange (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: RecordDirectives' a -> Range Source #

HasRange a => HasRange (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: WithHiding a -> Range Source #

HasRange a => HasRange (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: WithOrigin a -> Range Source #

HasRange a => HasRange (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: FieldAssignment' a -> Range Source #

HasRange e => HasRange (OpApp e) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: OpApp e -> Range Source #

HasRange (TacticAttribute' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: TacticAttribute' a -> Range Source #

IsExpr e => HasRange (ExprView e) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Operators.Parser

Methods

getRange :: ExprView e -> Range Source #

HasRange (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: DefInfo' t -> Range Source #

HasRange a => HasRange (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: PrintRange a -> Range Source #

HasRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: TopLevelModuleName' Range -> Range Source #

HasRange a => HasRange (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Closure a -> Range Source #

HasRange a => HasRange (List1 a) Source #

Precondition: The ranges of the list elements must point to the same file (or be empty).

Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: List1 a -> Range Source #

HasRange a => HasRange (List2 a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: List2 a -> Range Source #

HasRange a => HasRange (Set1 a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Set1 a -> Range Source #

HasRange a => HasRange (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Maybe a -> Range Source #

HasRange a => HasRange [a] Source #

Precondition: The ranges of the list elements must point to the same file (or be empty).

Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: [a] -> Range Source #

(HasRange a, HasRange b) => HasRange (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: ImportDirective' a b -> Range Source #

(HasRange a, HasRange b) => HasRange (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: ImportedName' a b -> Range Source #

HasRange a => HasRange (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Named name a -> Range Source #

(HasRange a, HasRange b) => HasRange (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Renaming' a b -> Range Source #

(HasRange a, HasRange b) => HasRange (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Using' a b -> Range Source #

HasRange a => HasRange (Dom' t a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getRange :: Dom' t a -> Range Source #

(HasRange a, HasRange b) => HasRange (Either a b) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Either a b -> Range Source #

(HasRange a, HasRange b) => HasRange (a, b) Source #

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: (a, b) -> Range Source #

(HasRange a, HasRange b, HasRange c) => HasRange (a, b, c) Source #

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: (a, b, c) -> Range Source #

(HasRange qn, HasRange nm, HasRange p, HasRange e) => HasRange (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: RewriteEqn' qn nm p e -> Range Source #

(HasRange a, HasRange b, HasRange c, HasRange d) => HasRange (a, b, c, d) Source #

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: (a, b, c, d) -> Range Source #

(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e) => HasRange (a, b, c, d, e) Source #

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: (a, b, c, d, e) -> Range Source #

(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f) => HasRange (a, b, c, d, e, f) Source #

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: (a, b, c, d, e, f) -> Range Source #

(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f, HasRange g) => HasRange (a, b, c, d, e, f, g) Source #

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: (a, b, c, d, e, f, g) -> Range Source #

class HasRangeWithoutFile a where Source #

Things that have a RangeWithoutFile are instances of this class.

Minimal complete definition

Nothing

Methods

getRangeWithoutFile :: a -> RangeWithoutFile Source #

default getRangeWithoutFile :: forall (t :: Type -> Type) b. (Foldable t, HasRangeWithoutFile b, t b ~ a) => a -> RangeWithoutFile Source #

Instances

Instances details
HasRangeWithoutFile Layer Source # 
Instance details

Defined in Agda.Syntax.Parser.Literate

Methods

getRangeWithoutFile :: Layer -> RangeWithoutFile Source #

HasRangeWithoutFile Token Source # 
Instance details

Defined in Agda.Syntax.Parser.Tokens

Methods

getRangeWithoutFile :: Token -> RangeWithoutFile Source #

HasRangeWithoutFile IntervalWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: IntervalWithoutFile -> RangeWithoutFile Source #

HasRangeWithoutFile RangeWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: RangeWithoutFile -> RangeWithoutFile Source #

HasRangeWithoutFile () Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: () -> RangeWithoutFile Source #

HasRangeWithoutFile Bool Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: Bool -> RangeWithoutFile Source #

HasRangeWithoutFile a => HasRangeWithoutFile (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: List1 a -> RangeWithoutFile Source #

HasRangeWithoutFile a => HasRangeWithoutFile (List2 a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: List2 a -> RangeWithoutFile Source #

HasRangeWithoutFile a => HasRangeWithoutFile (Set1 a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: Set1 a -> RangeWithoutFile Source #

HasRangeWithoutFile a => HasRangeWithoutFile (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: Maybe a -> RangeWithoutFile Source #

HasRangeWithoutFile a => HasRangeWithoutFile [a] Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: [a] -> RangeWithoutFile Source #

(HasRangeWithoutFile a, HasRangeWithoutFile b) => HasRangeWithoutFile (Either a b) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: Either a b -> RangeWithoutFile Source #

(HasRangeWithoutFile a, HasRangeWithoutFile b) => HasRangeWithoutFile (a, b) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: (a, b) -> RangeWithoutFile Source #

(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c) => HasRangeWithoutFile (a, b, c) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: (a, b, c) -> RangeWithoutFile Source #

(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d) => HasRangeWithoutFile (a, b, c, d) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: (a, b, c, d) -> RangeWithoutFile Source #

(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d, HasRangeWithoutFile e) => HasRangeWithoutFile (a, b, c, d, e) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: (a, b, c, d, e) -> RangeWithoutFile Source #

(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d, HasRangeWithoutFile e, HasRangeWithoutFile f) => HasRangeWithoutFile (a, b, c, d, e, f) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: (a, b, c, d, e, f) -> RangeWithoutFile Source #

(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d, HasRangeWithoutFile e, HasRangeWithoutFile f, HasRangeWithoutFile g) => HasRangeWithoutFile (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRangeWithoutFile :: (a, b, c, d, e, f, g) -> RangeWithoutFile Source #

class HasRange a => SetRange a where Source #

If it is also possible to set the range, this is the class.

Instances should satisfy getRange (setRange r x) == r.

Minimal complete definition

Nothing

Methods

setRange :: Range -> a -> a Source #

default setRange :: forall (f :: Type -> Type) b. (Functor f, SetRange b, f b ~ a) => Range -> a -> a Source #

Instances

Instances details
SetRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

setRange :: Range -> BindName -> BindName Source #

SetRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> ModuleName -> ModuleName Source #

SetRange Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> Name -> Name Source #

SetRange QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> QName -> QName Source #

SetRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Cohesion -> Cohesion Source #

SetRange NotationPart Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> NotationPart -> NotationPart Source #

SetRange OriginIrrelevant Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> OriginIrrelevant -> OriginIrrelevant Source #

SetRange OriginRelevant Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> OriginRelevant -> OriginRelevant Source #

SetRange OriginShapeIrrelevant Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> OriginShapeIrrelevant -> OriginShapeIrrelevant Source #

SetRange PolarityModality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> PolarityModality -> PolarityModality Source #

SetRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Q0Origin -> Q0Origin Source #

SetRange