Agda.Syntax.Position

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

Positions

type Position = Position' SrcFile

type PositionWithoutFile = Position' ()

data Position' a

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

• srcFile :: !a

  File.

• posPos :: !Int32

  Position, counting from 1.

• posLine :: !Int32

  Line number, counting from 1.

• posCol :: !Int32

  Column number, counting from 1.

Instances

Pretty PositionWithoutFile

Defined in Agda.Syntax.Position

Methods

pretty :: PositionWithoutFile -> Doc

prettyPrec :: Int -> PositionWithoutFile -> Doc

prettyList :: [PositionWithoutFile] -> Doc

Foldable Position'

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'

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'

Defined in Agda.Syntax.Position

Methods

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

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

NFData Position

Defined in Agda.Syntax.Position

Methods

rnf :: Position -> ()

NFData PositionWithoutFile

Defined in Agda.Syntax.Position

Methods

rnf :: PositionWithoutFile -> ()

EncodeTCM (Position' ())

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Position' () -> TCM Value

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

Defined in Agda.Syntax.Position

Methods

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

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

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

EmbPrj a => EmbPrj (Position' a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Position' a -> S Int32

icod_ :: Position' a -> S Int32

value :: Int32 -> R (Position' a)

Generic (Position' a)

Defined in Agda.Syntax.Position

Associated Types

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

Methods

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

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

Read a => Read (Position' a)

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)

Defined in Agda.Syntax.Position

Methods

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

show :: Position' a -> String

showList :: [Position' a] -> ShowS

Eq a => Eq (Position' a)

Defined in Agda.Syntax.Position

Methods

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

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

Ord a => Ord (Position' a)

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

ToJSON (Position' ())

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: Position' () -> Value

toEncoding :: Position' () -> Encoding

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

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

omitField :: Position' () -> Bool

type Rep (Position' a)

Defined in Agda.Syntax.Position

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

type SrcFile = Maybe RangeFile

data RangeFile

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

Constructors

RangeFile

Fields

• rangeFilePath :: !AbsolutePath

  The file's path.

• rangeFileName :: !(Maybe TopLevelModuleName)

  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 should not contain a range.

Instances

EncodeTCM Range

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Range -> TCM Value

Pretty RangeFile

Defined in Agda.Syntax.Position

Methods

pretty :: RangeFile -> Doc

prettyPrec :: Int -> RangeFile -> Doc

prettyList :: [RangeFile] -> Doc

HasRange Interval

Defined in Agda.Syntax.Position

Methods

getRange :: Interval -> Range

HasRange Range

Defined in Agda.Syntax.Position

Methods

getRange :: Range -> Range

KillRange Range

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Range

SetRange Range

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> Range -> Range

FreshName Range

Defined in Agda.TypeChecking.Monad.Base

Methods

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

PrettyTCM Range

Defined in Agda.TypeChecking.Pretty

Methods

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

EmbPrj Range

Ranges are always deserialised as noRange.

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Range -> S Int32

icod_ :: Range -> S Int32

value :: Int32 -> R Range

EmbPrj RangeFile

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: RangeFile -> S Int32

icod_ :: RangeFile -> S Int32

value :: Int32 -> R RangeFile

Subst Range

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Range

Methods

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

Generic RangeFile

Defined in Agda.Syntax.Position

Associated Types

type Rep RangeFile :: Type -> Type

Methods

from :: RangeFile -> Rep RangeFile x

to :: Rep RangeFile x -> RangeFile

Read RangeFile

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

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS RangeFile

readList :: ReadS [RangeFile]

readPrec :: ReadPrec RangeFile

readListPrec :: ReadPrec [RangeFile]

Show RangeFile

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> RangeFile -> ShowS

show :: RangeFile -> String

showList :: [RangeFile] -> ShowS

NFData Interval

Defined in Agda.Syntax.Position

Methods

rnf :: Interval -> ()

NFData Position

Defined in Agda.Syntax.Position

Methods

rnf :: Position -> ()

NFData RangeFile

Defined in Agda.Syntax.Position

Methods

rnf :: RangeFile -> ()

Eq RangeFile

Only the rangeFileName component is compared.

Defined in Agda.Syntax.Position

Methods

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

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

Ord RangeFile

Only the rangeFileName component is compared.

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

ToJSON Range

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: Range -> Value

toEncoding :: Range -> Encoding

toJSONList :: [Range] -> Value

toEncodingList :: [Range] -> Encoding

omitField :: Range -> Bool

LensClosure MetaInfo Range

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' MetaInfo (Closure Range)

LensClosure MetaVariable Range

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' MetaVariable (Closure Range)

FreshName (Range, String)

Defined in Agda.TypeChecking.Monad.Base

Methods

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

type SubstArg Range

Defined in Agda.TypeChecking.Substitute

type SubstArg Range = Term

type Rep RangeFile

Defined in Agda.Syntax.Position

type Rep RangeFile = D1 ('MetaData "RangeFile" "Agda.Syntax.Position" "Agda-2.6.3.20230930-inplace" '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))))

mkRangeFile :: AbsolutePath -> Maybe TopLevelModuleName -> RangeFile

A smart constructor for RangeFile.

positionInvariant :: Position' a -> Bool

startPos :: Maybe RangeFile -> Position

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

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

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

Advance the position by a string.

movePosByString = foldl' movePos

backupPos :: Position' a -> Position' a

Backup the position by one character.

Precondition: The character must not be 'n'.

startPos' :: a -> Position' a

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

Intervals

type Interval = Interval' SrcFile

type IntervalWithoutFile = Interval' ()

data Interval' a

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

Note the invariant which intervals have to satisfy: intervalInvariant.

Constructors

Interval

Fields

• iStart, iEnd :: !(Position' a)

Instances

Pretty IntervalWithoutFile

Defined in Agda.Syntax.Position

Methods

pretty :: IntervalWithoutFile -> Doc

prettyPrec :: Int -> IntervalWithoutFile -> Doc

prettyList :: [IntervalWithoutFile] -> Doc

HasRange Interval

Defined in Agda.Syntax.Position

Methods

getRange :: Interval -> Range

Foldable Interval'

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'

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'

Defined in Agda.Syntax.Position

Methods

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

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

NFData Interval

Defined in Agda.Syntax.Position

Methods

rnf :: Interval -> ()

NFData IntervalWithoutFile

Defined in Agda.Syntax.Position

Methods

rnf :: IntervalWithoutFile -> ()

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

Defined in Agda.Syntax.Position

Methods

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

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

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

EmbPrj a => EmbPrj (Interval' a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Interval' a -> S Int32

icod_ :: Interval' a -> S Int32

value :: Int32 -> R (Interval' a)

Generic (Interval' a)

Defined in Agda.Syntax.Position

Associated Types

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

Methods

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

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

Read a => Read (Interval' a)

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)

Defined in Agda.Syntax.Position

Methods

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

show :: Interval' a -> String

showList :: [Interval' a] -> ShowS

Eq a => Eq (Interval' a)

Defined in Agda.Syntax.Position

Methods

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

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

Ord a => Ord (Interval' a)

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)

Defined in Agda.Syntax.Position

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

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

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

Converts a file name and two positions to an interval.

getIntervalFile :: Interval' a -> a

Gets the srcFile component of the interval. Because of the invariant, they are both the same.

iLength :: Interval' a -> Int32

The length of an interval.

fuseIntervals :: Ord a => Interval' a -> Interval' a -> Interval' a

Finds the least interval which covers the arguments.

Precondition: The intervals must point to the same file.

setIntervalFile :: a -> Interval' b -> Interval' a

Sets the srcFile components of the interval.

Ranges

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

EncodeTCM Range

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Range -> TCM Value

HasRange Range

Defined in Agda.Syntax.Position

Methods

getRange :: Range -> Range

KillRange Range

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Range

SetRange Range

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> Range -> Range

FreshName Range

Defined in Agda.TypeChecking.Monad.Base

Methods

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

PrettyTCM Range

Defined in Agda.TypeChecking.Pretty

Methods

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

EmbPrj Range

Ranges are always deserialised as noRange.

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Range -> S Int32

icod_ :: Range -> S Int32

value :: Int32 -> R Range

Subst Range

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Range

Methods

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

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)

Functor Range'

Defined in Agda.Syntax.Position

Methods

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

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

ToJSON Range

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: Range -> Value

toEncoding :: Range -> Encoding

toJSONList :: [Range] -> Value

toEncodingList :: [Range] -> Encoding

omitField :: Range -> Bool

LensClosure MetaInfo Range

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' MetaInfo (Closure Range)

LensClosure MetaVariable Range

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' MetaVariable (Closure Range)

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

Eq a => Monoid (Range' a)

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)

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)

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

Read a => Read (Range' a)

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

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)

Defined in Agda.Syntax.Position

Methods

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

show :: Range' a -> String

showList :: [Range' a] -> ShowS

NFData a => NFData (Range' a)

Defined in Agda.Syntax.Position

Methods

rnf :: Range' a -> ()

Eq a => Eq (Range' a)

Defined in Agda.Syntax.Position

Methods

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

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

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

FreshName (Range, String)

Defined in Agda.TypeChecking.Monad.Base

Methods

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

type SubstArg Range

Defined in Agda.TypeChecking.Substitute

type SubstArg Range = Term

type Rep (Range' a)

Defined in Agda.Syntax.Position

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

Range invariant.

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

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

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

Precondition: consecutiveAndSeparated.

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

Converts a file name and an interval to a range.

rangeIntervals :: Range' a -> [IntervalWithoutFile]

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

rangeFile :: Range -> SrcFile

The file the range is pointing to.

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

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

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

rightMargin :: Range -> Range

Conflate a range to its right margin.

noRange :: Range' a

Ranges between two unknown positions

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

Converts two positions to a range.

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

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

Converts a file name and two positions to a range.

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

The initial position in the range, if any.

rStart' :: Range' a -> Maybe PositionWithoutFile

The initial position in the range, if any.

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

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

rEnd' :: Range' a -> Maybe PositionWithoutFile

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

rangeToInterval :: Range' a -> Maybe IntervalWithoutFile

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

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

Converts a range to an interval, if possible.

continuous :: Range' a -> Range' a

Returns the shortest continuous range containing the given one.

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

Removes gaps between intervals on the same line.

newtype PrintRange a

Wrapper to indicate that range should be printed.

Constructors

PrintRange a

Instances

(Pretty a, HasRange a) => Pretty (PrintRange a)

Defined in Agda.Syntax.Position

Methods

pretty :: PrintRange a -> Doc

prettyPrec :: Int -> PrintRange a -> Doc

prettyList :: [PrintRange a] -> Doc

HasRange a => HasRange (PrintRange a)

Defined in Agda.Syntax.Position

Methods

getRange :: PrintRange a -> Range

KillRange a => KillRange (PrintRange a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (PrintRange a)

SetRange a => SetRange (PrintRange a)

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> PrintRange a -> PrintRange a

Eq a => Eq (PrintRange a)

Defined in Agda.Syntax.Position

Methods

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

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

Ord a => Ord (PrintRange a)

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

Things that have a range are instances of this class.

Minimal complete definition

Nothing

Methods

getRange :: a -> Range

default getRange :: (Foldable t, HasRange b, t b ~ a) => a -> Range

Instances

HasRange HaskellPragma

Defined in Agda.Compiler.MAlonzo.Pragmas

Methods

getRange :: HaskellPragma -> Range

HasRange BindName

Defined in Agda.Syntax.Abstract

Methods

getRange :: BindName -> Range

HasRange Declaration

Defined in Agda.Syntax.Abstract

Methods

getRange :: Declaration -> Range

HasRange Expr

Defined in Agda.Syntax.Abstract

Methods

getRange :: Expr -> Range

HasRange LHS

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHS -> Range

HasRange LamBinding

Defined in Agda.Syntax.Abstract

Methods

getRange :: LamBinding -> Range

HasRange LetBinding

Defined in Agda.Syntax.Abstract

Methods

getRange :: LetBinding -> Range

HasRange RHS

Defined in Agda.Syntax.Abstract

Methods

getRange :: RHS -> Range

HasRange SpineLHS

Defined in Agda.Syntax.Abstract

Methods

getRange :: SpineLHS -> Range

HasRange TypedBinding

Defined in Agda.Syntax.Abstract

Methods

getRange :: TypedBinding -> Range

HasRange WhereDeclarations

Defined in Agda.Syntax.Abstract

Methods

getRange :: WhereDeclarations -> Range

HasRange AmbiguousQName

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

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: AmbiguousQName -> Range

HasRange ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: ModuleName -> Range

HasRange Name

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: Name -> Range

HasRange QName

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: QName -> Range

HasRange Access

Defined in Agda.Syntax.Common

Methods

getRange :: Access -> Range

HasRange Annotation

Defined in Agda.Syntax.Common

Methods

getRange :: Annotation -> Range

HasRange ArgInfo

Defined in Agda.Syntax.Common

Methods

getRange :: ArgInfo -> Range

HasRange Cohesion

Defined in Agda.Syntax.Common

Methods

getRange :: Cohesion -> Range

HasRange Erased

Defined in Agda.Syntax.Common

Methods

getRange :: Erased -> Range

HasRange Fixity

Defined in Agda.Syntax.Common

Methods

getRange :: Fixity -> Range

HasRange Hiding

Defined in Agda.Syntax.Common

Methods

getRange :: Hiding -> Range

HasRange IsInstance

Defined in Agda.Syntax.Common

Methods

getRange :: IsInstance -> Range

HasRange IsMacro

Defined in Agda.Syntax.Common

Methods

getRange :: IsMacro -> Range

HasRange Modality

Defined in Agda.Syntax.Common

Methods

getRange :: Modality -> Range

HasRange NotationPart

Defined in Agda.Syntax.Common

Methods

getRange :: NotationPart -> Range

HasRange Origin

Defined in Agda.Syntax.Common

Methods

getRange :: Origin -> Range

HasRange PatternOrCopattern

Defined in Agda.Syntax.Common

Methods

getRange :: PatternOrCopattern -> Range

HasRange Q0Origin

Defined in Agda.Syntax.Common

Methods

getRange :: Q0Origin -> Range

HasRange Q1Origin

Defined in Agda.Syntax.Common

Methods

getRange :: Q1Origin -> Range

HasRange Quantity

Defined in Agda.Syntax.Common

Methods

getRange :: Quantity -> Range

HasRange QωOrigin

Defined in Agda.Syntax.Common

Methods

getRange :: QωOrigin -> Range

HasRange Relevance

Defined in Agda.Syntax.Common

Methods

getRange :: Relevance -> Range

HasRange Induction

Defined in Agda.Syntax.Common

Methods

getRange :: Induction -> Range

HasRange AsName

Defined in Agda.Syntax.Concrete

Methods

getRange :: AsName -> Range

HasRange Binder

Defined in Agda.Syntax.Concrete

Methods

getRange :: Binder -> Range

HasRange BoundName

Defined in Agda.Syntax.Concrete

Methods

getRange :: BoundName -> Range

HasRange Declaration

Defined in Agda.Syntax.Concrete

Methods

getRange :: Declaration -> Range

HasRange DoStmt

Defined in Agda.Syntax.Concrete

Methods

getRange :: DoStmt -> Range

HasRange Expr

Defined in Agda.Syntax.Concrete

Methods

getRange :: Expr -> Range

HasRange LHS

Defined in Agda.Syntax.Concrete

Methods

getRange :: LHS -> Range

HasRange LHSCore

Defined in Agda.Syntax.Concrete

Methods

getRange :: LHSCore -> Range

HasRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamBinding -> Range

HasRange LamClause

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamClause -> Range

HasRange ModuleApplication

Defined in Agda.Syntax.Concrete

Methods

getRange :: ModuleApplication -> Range

HasRange ModuleAssignment

Defined in Agda.Syntax.Concrete

Methods

getRange :: ModuleAssignment -> Range

HasRange Pattern

Defined in Agda.Syntax.Concrete

Methods

getRange :: Pattern -> Range

HasRange Pragma

Defined in Agda.Syntax.Concrete

Methods

getRange :: Pragma -> Range

HasRange RHS

Defined in Agda.Syntax.Concrete

Methods

getRange :: RHS -> Range

HasRange RecordDirective

Defined in Agda.Syntax.Concrete

Methods

getRange :: RecordDirective -> Range

HasRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: TypedBinding -> Range

HasRange WhereClause

Defined in Agda.Syntax.Concrete

Methods

getRange :: WhereClause -> Range

HasRange Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

getRange :: Attribute -> Range

HasRange DeclarationException

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationException -> Range

HasRange DeclarationException'

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationException' -> Range

HasRange DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationWarning -> Range

HasRange DeclarationWarning'

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationWarning' -> Range

HasRange NiceDeclaration

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

getRange :: NiceDeclaration -> Range

HasRange Name

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: Name -> Range

HasRange QName

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: QName -> Range

HasRange AppInfo

Defined in Agda.Syntax.Info

Methods

getRange :: AppInfo -> Range

HasRange ConPatInfo

Defined in Agda.Syntax.Info

Methods

getRange :: ConPatInfo -> Range

HasRange DeclInfo

Defined in Agda.Syntax.Info

Methods

getRange :: DeclInfo -> Range

HasRange ExprInfo

Defined in Agda.Syntax.Info

Methods

getRange :: ExprInfo -> Range

HasRange LHSInfo

Defined in Agda.Syntax.Info

Methods

getRange :: LHSInfo -> Range

HasRange LetInfo

Defined in Agda.Syntax.Info

Methods

getRange :: LetInfo -> Range

HasRange MetaInfo

Defined in Agda.Syntax.Info

Methods

getRange :: MetaInfo -> Range

HasRange ModuleInfo

Defined in Agda.Syntax.Info

Methods

getRange :: ModuleInfo -> Range

HasRange MutualInfo

Defined in Agda.Syntax.Info

Methods

getRange :: MutualInfo -> Range

HasRange PatInfo

Defined in Agda.Syntax.Info

Methods

getRange :: PatInfo -> Range

HasRange Clause

Defined in Agda.Syntax.Internal

Methods

getRange :: Clause -> Range

HasRange ConHead

Defined in Agda.Syntax.Internal

Methods

getRange :: ConHead -> Range

HasRange Layer

Defined in Agda.Syntax.Parser.Literate

Methods

getRange :: Layer -> Range

HasRange ParseError

Defined in Agda.Syntax.Parser.Monad

Methods

getRange :: ParseError -> Range

HasRange ParseWarning

Defined in Agda.Syntax.Parser.Monad

Methods

getRange :: ParseWarning -> Range

HasRange Token

Defined in Agda.Syntax.Parser.Tokens

Methods

getRange :: Token -> Range

HasRange Interval

Defined in Agda.Syntax.Position

Methods

getRange :: Interval -> Range

HasRange Range

Defined in Agda.Syntax.Position

Methods

getRange :: Range -> Range

HasRange AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

getRange :: AbstractName -> Range

HasRange RawTopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Methods

getRange :: RawTopLevelModuleName -> Range

HasRange TopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Methods

getRange :: TopLevelModuleName -> Range

HasRange Call

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Call -> Range

HasRange CallInfo

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: CallInfo -> Range

HasRange CompilerPragma

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: CompilerPragma -> Range

HasRange Constraint

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Constraint -> Range

HasRange MetaInfo

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: MetaInfo -> Range

HasRange MetaVariable

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: MetaVariable -> Range

HasRange ProblemConstraint

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: ProblemConstraint -> Range

HasRange TCErr

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: TCErr -> Range

HasRange TCWarning

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: TCWarning -> Range

HasRange Item

Defined in Agda.TypeChecking.Positivity

Methods

getRange :: Item -> Range

HasRange ()

Defined in Agda.Syntax.Position

Methods

getRange :: () -> Range

HasRange Bool

Defined in Agda.Syntax.Position

Methods

getRange :: Bool -> Range

HasRange a => HasRange (Binder' a)

Defined in Agda.Syntax.Abstract

Methods

getRange :: Binder' a -> Range

HasRange a => HasRange (Clause' a)

Defined in Agda.Syntax.Abstract

Methods

getRange :: Clause' a -> Range

HasRange (LHSCore' e)

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHSCore' e -> Range

HasRange (Pattern' e)

Defined in Agda.Syntax.Abstract

Methods

getRange :: Pattern' e -> Range

HasRange a => HasRange (Arg a)

Defined in Agda.Syntax.Common

Methods

getRange :: Arg a -> Range

HasRange a => HasRange (HasEta' a)

Defined in Agda.Syntax.Common

Methods

getRange :: HasEta' a -> Range

HasRange a => HasRange (MaybePlaceholder a)

Defined in Agda.Syntax.Common

Methods

getRange :: MaybePlaceholder a -> Range

HasRange (Ranged a)

Defined in Agda.Syntax.Common

Methods

getRange :: Ranged a -> Range

HasRange a => HasRange (RecordDirectives' a)

Defined in Agda.Syntax.Common

Methods

getRange :: RecordDirectives' a -> Range

HasRange a => HasRange (WithHiding a)

Defined in Agda.Syntax.Common

Methods

getRange :: WithHiding a -> Range

HasRange a => HasRange (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

getRange :: WithOrigin a -> Range

HasRange a => HasRange (FieldAssignment' a)

Defined in Agda.Syntax.Concrete

Methods

getRange :: FieldAssignment' a -> Range

HasRange e => HasRange (OpApp e)

Defined in Agda.Syntax.Concrete

Methods

getRange :: OpApp e -> Range

IsExpr e => HasRange (ExprView e)

Defined in Agda.Syntax.Concrete.Operators.Parser

Methods

getRange :: ExprView e -> Range

HasRange (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

getRange :: DefInfo' t -> Range

HasRange a => HasRange (PrintRange a)

Defined in Agda.Syntax.Position

Methods

getRange :: PrintRange a -> Range

HasRange a => HasRange (Closure a)

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Closure a -> Range

HasRange a => HasRange (List1 a)

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

Defined in Agda.Syntax.Position

Methods

getRange :: List1 a -> Range

HasRange a => HasRange (List2 a)

Defined in Agda.Syntax.Position

Methods

getRange :: List2 a -> Range

HasRange a => HasRange (Maybe a)

Defined in Agda.Syntax.Position

Methods

getRange :: Maybe a -> Range

HasRange a => HasRange [a]

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

Defined in Agda.Syntax.Position

Methods

getRange :: [a] -> Range

(HasRange a, HasRange b) => HasRange (ImportDirective' a b)

Defined in Agda.Syntax.Common

Methods

getRange :: ImportDirective' a b -> Range

(HasRange a, HasRange b) => HasRange (ImportedName' a b)

Defined in Agda.Syntax.Common

Methods

getRange :: ImportedName' a b -> Range

HasRange a => HasRange (Named name a)

Defined in Agda.Syntax.Common

Methods

getRange :: Named name a -> Range

(HasRange a, HasRange b) => HasRange (Renaming' a b)

Defined in Agda.Syntax.Common

Methods

getRange :: Renaming' a b -> Range

(HasRange a, HasRange b) => HasRange (Using' a b)

Defined in Agda.Syntax.Common

Methods

getRange :: Using' a b -> Range

HasRange a => HasRange (Dom' t a)

Defined in Agda.Syntax.Internal

Methods

getRange :: Dom' t a -> Range

(HasRange a, HasRange b) => HasRange (Either a b)

Defined in Agda.Syntax.Position

Methods

getRange :: Either a b -> Range

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

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

Defined in Agda.Syntax.Position

Methods

getRange :: (a, b) -> Range

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

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

Defined in Agda.Syntax.Position

Methods

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

(HasRange qn, HasRange nm, HasRange p, HasRange e) => HasRange (RewriteEqn' qn nm p e)

Defined in Agda.Syntax.Common

Methods

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

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

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

Defined in Agda.Syntax.Position

Methods

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

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

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

Defined in Agda.Syntax.Position

Methods

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

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

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

Defined in Agda.Syntax.Position

Methods

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

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

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

Defined in Agda.Syntax.Position

Methods

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

class HasRange a => SetRange a where

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

default setRange :: (Functor f, SetRange b, f b ~ a) => Range -> a -> a

Instances

SetRange BindName

Defined in Agda.Syntax.Abstract

Methods

setRange :: Range -> BindName -> BindName

SetRange ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> ModuleName -> ModuleName

SetRange Name

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> Name -> Name

SetRange QName

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> QName -> QName

SetRange Cohesion

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Cohesion -> Cohesion

SetRange NotationPart

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> NotationPart -> NotationPart

SetRange Q0Origin

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Q0Origin -> Q0Origin

SetRange Q1Origin

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Q1Origin -> Q1Origin

SetRange Quantity

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Quantity -> Quantity

SetRange QωOrigin

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> QωOrigin -> QωOrigin

SetRange Relevance

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Relevance -> Relevance

SetRange Pattern

Defined in Agda.Syntax.Concrete

Methods

setRange :: Range -> Pattern -> Pattern

SetRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

setRange :: Range -> TypedBinding -> TypedBinding

SetRange Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

setRange :: Range -> Attribute -> Attribute

SetRange Name

Defined in Agda.Syntax.Concrete.Name

Methods

setRange :: Range -> Name -> Name

SetRange QName

Defined in Agda.Syntax.Concrete.Name

Methods

setRange :: Range -> QName -> QName

SetRange ConPatInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> ConPatInfo -> ConPatInfo

SetRange DeclInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> DeclInfo -> DeclInfo

SetRange ModuleInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> ModuleInfo -> ModuleInfo

SetRange PatInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> PatInfo -> PatInfo

SetRange ConHead

Defined in Agda.Syntax.Internal

Methods

setRange :: Range -> ConHead -> ConHead

SetRange Range

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> Range -> Range

SetRange AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

setRange :: Range -> AbstractName -> AbstractName

SetRange RawTopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Methods

setRange :: Range -> RawTopLevelModuleName -> RawTopLevelModuleName

SetRange TopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Methods

setRange :: Range -> TopLevelModuleName -> TopLevelModuleName

SetRange MetaInfo

Defined in Agda.TypeChecking.Monad.Base

Methods

setRange :: Range -> MetaInfo -> MetaInfo

SetRange MetaVariable

Defined in Agda.TypeChecking.Monad.Base

Methods

setRange :: Range -> MetaVariable -> MetaVariable

SetRange (Pattern' a)

Defined in Agda.Syntax.Abstract

Methods

setRange :: Range -> Pattern' a -> Pattern' a

SetRange a => SetRange (Arg a)

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Arg a -> Arg a

SetRange a => SetRange (WithHiding a)

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> WithHiding a -> WithHiding a

SetRange a => SetRange (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> WithOrigin a -> WithOrigin a

SetRange (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> DefInfo' t -> DefInfo' t

SetRange a => SetRange (PrintRange a)

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> PrintRange a -> PrintRange a

SetRange a => SetRange (Maybe a)

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> Maybe a -> Maybe a

SetRange a => SetRange [a]

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> [a] -> [a]

SetRange a => SetRange (Named name a)

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Named name a -> Named name a

class KillRange a where

Killing the range of an object sets all range information to noRange.

Minimal complete definition

Nothing

Methods

killRange :: KillRangeT a

default killRange :: (Functor f, KillRange b, f b ~ a) => KillRangeT a

Instances

KillRange BindName

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT BindName

KillRange DataDefParams

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT DataDefParams

KillRange Declaration

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT Declaration

KillRange Expr

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT Expr

KillRange GeneralizeTelescope

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT GeneralizeTelescope

KillRange LHS

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT LHS

KillRange LamBinding

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT LamBinding

KillRange LetBinding

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT LetBinding

KillRange ModuleApplication

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ModuleApplication

KillRange ProblemEq

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ProblemEq

KillRange RHS

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT RHS

KillRange ScopeCopyInfo

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ScopeCopyInfo

KillRange SpineLHS

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT SpineLHS

KillRange TypedBinding

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT TypedBinding

KillRange TypedBindingInfo

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT TypedBindingInfo

KillRange WhereDeclarations

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT WhereDeclarations

KillRange AmbiguousQName

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT AmbiguousQName

KillRange ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT ModuleName

KillRange Name

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT Name

KillRange QName

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT QName

KillRange Suffix

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT Suffix

KillRange BuiltinId

Defined in Agda.Syntax.Builtin

Methods

killRange :: KillRangeT BuiltinId

KillRange PrimitiveId

Defined in Agda.Syntax.Builtin

Methods

killRange :: KillRangeT PrimitiveId

KillRange Access

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Access

KillRange Annotation

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Annotation

KillRange ArgInfo

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT ArgInfo

KillRange Cohesion

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Cohesion

KillRange ConOrigin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT ConOrigin

KillRange CoverageCheck

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT CoverageCheck

KillRange Erased

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Erased

KillRange ExpandedEllipsis

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT ExpandedEllipsis

KillRange Fixity

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Fixity

KillRange Fixity'

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Fixity'

KillRange FreeVariables

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT FreeVariables

KillRange Hiding

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Hiding

KillRange InteractionId

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT InteractionId

KillRange IsAbstract

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT IsAbstract

KillRange IsInstance

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT IsInstance

KillRange IsMacro

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT IsMacro

KillRange IsOpaque

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT IsOpaque

KillRange Language

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Language

KillRange Modality

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Modality

KillRange NameId

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT NameId

KillRange NotationPart

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT NotationPart

KillRange OpaqueId

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT OpaqueId

KillRange Origin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Origin

KillRange PatternOrCopattern

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT PatternOrCopattern

KillRange PositivityCheck

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT PositivityCheck

KillRange ProjOrigin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT ProjOrigin

KillRange Q0Origin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Q0Origin

KillRange Q1Origin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Q1Origin

KillRange Quantity

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Quantity

KillRange QωOrigin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT QωOrigin

KillRange Relevance

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Relevance

KillRange UniverseCheck

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT UniverseCheck

KillRange Induction

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Induction

KillRange AsName

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT AsName

KillRange Binder

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Binder

KillRange BoundName

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT BoundName

KillRange Declaration

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Declaration

KillRange DoStmt

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT DoStmt

KillRange Expr

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Expr

KillRange LHS

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LHS

KillRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LamBinding

KillRange LamClause

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LamClause

KillRange ModuleApplication

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT ModuleApplication

KillRange ModuleAssignment

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT ModuleAssignment

KillRange Pattern

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Pattern

KillRange Pragma

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Pragma

KillRange RHS

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT RHS

KillRange RecordDirective

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT RecordDirective

KillRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT TypedBinding

KillRange WhereClause

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT WhereClause

KillRange Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

killRange :: KillRangeT Attribute

KillRange Name

Defined in Agda.Syntax.Concrete.Name

Methods

killRange :: KillRangeT Name

KillRange QName

Defined in Agda.Syntax.Concrete.Name

Methods

killRange :: KillRangeT QName

KillRange AppInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT AppInfo

KillRange ConPatInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT ConPatInfo

KillRange DeclInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT DeclInfo

KillRange ExprInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT ExprInfo

KillRange LHSInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT LHSInfo

KillRange LetInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT LetInfo

KillRange MetaInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT MetaInfo

KillRange ModuleInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT ModuleInfo

KillRange MutualInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT MutualInfo

KillRange PatInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT PatInfo

KillRange Clause

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Clause

KillRange ConHead

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT ConHead

KillRange ConPatternInfo

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT ConPatternInfo

KillRange DBPatVar

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT DBPatVar

KillRange DataOrRecord

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT DataOrRecord

KillRange Level

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Level

KillRange PatOrigin

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PatOrigin

KillRange PatternInfo

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PatternInfo

KillRange PlusLevel

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PlusLevel

KillRange Sort

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Sort

KillRange Substitution

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Substitution

KillRange Term

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Term

KillRange Literal

Defined in Agda.Syntax.Literal

Methods

killRange :: KillRangeT Literal

KillRange Range

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Range

KillRange ScopeInfo

Defined in Agda.Syntax.Scope.Base

Methods

killRange :: KillRangeT ScopeInfo

KillRange RawTopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Methods

killRange :: KillRangeT RawTopLevelModuleName

KillRange TopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Methods

killRange :: KillRangeT TopLevelModuleName

KillRange Compiled

Defined in Agda.Syntax.Treeless

Methods

killRange :: KillRangeT Compiled

KillRange CompiledClauses

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT CompiledClauses

KillRange SplitTag

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

killRange :: KillRangeT SplitTag

KillRange BuiltinSort

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT BuiltinSort

KillRange CompKit

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT CompKit

KillRange CompiledRepresentation

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT CompiledRepresentation

KillRange Definition

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Definition

KillRange Definitions

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Definitions

KillRange Defn

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Defn

KillRange DisplayForm

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT DisplayForm

KillRange DisplayTerm

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT DisplayTerm

KillRange DoGeneralize

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT DoGeneralize

KillRange EtaEquality

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT EtaEquality

KillRange ExtLamInfo

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT ExtLamInfo

KillRange FunctionFlag

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT FunctionFlag

KillRange IsForced

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT IsForced

KillRange MutualId

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT MutualId

KillRange NLPSort

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT NLPSort

KillRange NLPType

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT NLPType

KillRange NLPat

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT NLPat

KillRange NumGeneralizableArgs

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT NumGeneralizableArgs

KillRange Polarity

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Polarity

KillRange ProjLams

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT ProjLams

KillRange Projection

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Projection

KillRange ProjectionLikenessMissing

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT ProjectionLikenessMissing

KillRange RewriteRule

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT RewriteRule

KillRange RewriteRuleMap

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT RewriteRuleMap

KillRange Section

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Section

KillRange Sections

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Sections

KillRange Signature

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Signature

KillRange System

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT System

KillRange TermHead

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT TermHead

KillRange Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

killRange :: KillRangeT Occurrence

KillRange Permutation

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Permutation

KillRange Void

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Void

KillRange String

Overlaps with KillRange [a].

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT String

KillRange Integer

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Integer

KillRange ()

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT ()

KillRange Bool

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Bool

KillRange Int

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Int

KillRange a => KillRange (Binder' a)

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT (Binder' a)

KillRange a => KillRange (Clause' a)

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT (Clause' a)

KillRange e => KillRange (LHSCore' e)

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT (LHSCore' e)

KillRange e => KillRange (Pattern' e)

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT (Pattern' e)

KillRange a => KillRange (Arg a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Arg a)

KillRange a => KillRange (HasEta' a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (HasEta' a)

KillRange a => KillRange (MaybePlaceholder a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (MaybePlaceholder a)

KillRange (Ranged a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Ranged a)

KillRange a => KillRange (RecordDirectives' a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (RecordDirectives' a)

KillRange m => KillRange (TerminationCheck m)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (TerminationCheck m)

KillRange a => KillRange (WithHiding a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (WithHiding a)

KillRange a => KillRange (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (WithOrigin a)

KillRange a => KillRange (FieldAssignment' a)

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT (FieldAssignment' a)

KillRange e => KillRange (OpApp e)

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT (OpApp e)

KillRange x => KillRange (ThingWithFixity x)

Defined in Agda.Syntax.Fixity

Methods

killRange :: KillRangeT (ThingWithFixity x)

KillRange t => KillRange (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT (DefInfo' t)

KillRange a => KillRange (Abs a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Abs a)

KillRange a => KillRange (Blocked a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Blocked a)

KillRange a => KillRange (Pattern' a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Pattern' a)

KillRange a => KillRange (Tele a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Tele a)

KillRange a => KillRange (Type' a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Type' a)

KillRange a => KillRange (Elim' a)

Defined in Agda.Syntax.Internal.Elim

Methods

killRange :: KillRangeT (Elim' a)

KillRange a => KillRange (PrintRange a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (PrintRange a)

KillRange c => KillRange (Case c)

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT (Case c)

KillRange c => KillRange (WithArity c)

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT (WithArity c)

KillRange a => KillRange (SplitTree' a)

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

killRange :: KillRangeT (SplitTree' a)

KillRange a => KillRange (Closure a)

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT (Closure a)

KillRange c => KillRange (FunctionInverse' c)

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT (FunctionInverse' c)

KillRange a => KillRange (Open a)

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT (Open a)

KillRange a => KillRange (List1 a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (List1 a)

KillRange a => KillRange (List2 a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (List2 a)

KillRange a => KillRange (Drop a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Drop a)

(Ord a, KillRange a) => KillRange (Set a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Set a)

KillRange a => KillRange (Maybe a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Maybe a)

KillRange a => KillRange (Maybe a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Maybe a)

KillRange a => KillRange [a]

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT [a]

(KillRange a, KillRange b) => KillRange (ImportDirective' a b)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (ImportDirective' a b)

(KillRange a, KillRange b) => KillRange (ImportedName' a b)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (ImportedName' a b)

(KillRange name, KillRange a) => KillRange (Named name a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Named name a)

(KillRange a, KillRange b) => KillRange (Renaming' a b)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Renaming' a b)

(KillRange a, KillRange b) => KillRange (Using' a b)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Using' a b)

(KillRange t, KillRange a) => KillRange (Dom' t a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Dom' t a)

(KillRange a, KillRange b) => KillRange (Either a b)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Either a b)

KillRange a => KillRange (Map k a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Map k a)

(KillRange a, KillRange b) => KillRange (a, b)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (a, b)

(KillRange a, KillRange b, KillRange c) => KillRange (a, b, c)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (a, b, c)

(KillRange qn, KillRange nm, KillRange e, KillRange p) => KillRange (RewriteEqn' qn nm p e)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (RewriteEqn' qn nm p e)

(KillRange a, KillRange b, KillRange c, KillRange d) => KillRange (a, b, c, d)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (a, b, c, d)

type KillRangeT a = a -> a

killRangeMap :: (KillRange k, KillRange v) => KillRangeT (Map k v)

Remove ranges in keys and values of a map.

class KILLRANGE t b where

Methods

killRangeN :: IsBase t ~ b => All KillRange (Domains t) => t -> t

Instances

IsBase t ~ 'True => KILLRANGE t 'True

Defined in Agda.Syntax.Position

Methods

killRangeN :: t -> t

KILLRANGE t (IsBase t) => KILLRANGE (a -> t) 'False

Defined in Agda.Syntax.Position

Methods

killRangeN :: (a -> t) -> a -> t

withRangeOf :: (SetRange t, HasRange u) => t -> u -> t

x `withRangeOf` y sets the range of x to the range of y.

fuseRange :: (HasRange u, HasRange t) => u -> t -> Range

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

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

fuseRanges r r' unions the ranges r and r'.

Meaning it finds the least range r0 that covers r and r'.

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

beginningOf :: Range -> Range

beginningOf r is an empty range (a single, empty interval) positioned at the beginning of r. If r does not have a beginning, then noRange is returned.

beginningOfFile :: Range -> Range

beginningOfFile r is an empty range (a single, empty interval) at the beginning of r's starting position's file. If there is no such position, then an empty range is returned.

interleaveRanges :: HasRange a => [a] -> [a] -> ([a], [(a, a)])

Interleaves two streams of ranged elements

It will report the conflicts as a list of conflicting pairs. In case of conflict, the element with the earliest start position is placed first. In case of a tie, the element with the earliest ending position is placed first. If both tie, the element from the first list is placed first.