Agda-2.6.4.3: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Position

Description

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

Synopsis

Positions

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

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

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

Defined in Agda.Syntax.Common.Pretty

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

ToJSON (Position' ()) Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Generic (Position' a) Source # 
Instance details

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

Defined in Agda.Interaction.Base

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

Defined in Agda.Syntax.Position

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

type Rep (Position' a) Source # 
Instance details

Defined in Agda.Syntax.Position

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

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

Pretty RangeFile Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Pretty TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

HasRange Interval Source # 
Instance details

Defined in Agda.Syntax.Position

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

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

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

EmbPrj Range Source #

Ranges are always deserialised as noRange.

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj RangeFile Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Subst Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Range Source #

Sized TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

ToJSON Range Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Generic RangeFile Source # 
Instance details

Defined in Agda.Syntax.Position

Associated Types

type Rep RangeFile :: Type -> Type #

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

Show RangeFile Source # 
Instance details

Defined in Agda.Syntax.Position

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

Ord RangeFile Source #

Only the rangeFileName component is compared.

Instance details

Defined in Agda.Syntax.Position

LensClosure MetaInfo Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensClosure MetaVariable Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

SetRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

FreshName (Range, String) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type SubstArg Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type Rep RangeFile Source # 
Instance details

Defined in Agda.Syntax.Position

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

startPos :: Maybe RangeFile -> Position 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'.

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

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

Intervals

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 

Fields

Instances

Instances details
Pretty IntervalWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

HasRange Interval Source # 
Instance details

Defined in Agda.Syntax.Position

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

Generic (Interval' a) Source # 
Instance details

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

Defined in Agda.Interaction.Base

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

Defined in Agda.Syntax.Position

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

type Rep (Interval' a) Source # 
Instance details

Defined in Agda.Syntax.Position

type Rep (Interval' a) = D1 ('MetaData "Interval'" "Agda.Syntax.Position" "Agda-2.6.4.3-Ljl5wY0h7qEDjMk20qhhzf" '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))))

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

Converts a file name and two positions to an interval.

getIntervalFile :: Interval' a -> a Source #

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

iLength :: Interval' a -> Int32 Source #

The length of an interval.

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

Finds the least interval which covers the arguments.

Precondition: The intervals must point to the same file.

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

Sets the srcFile components of the interval.

Ranges

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

Pretty TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

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

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

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

EmbPrj Range Source #

Ranges are always deserialised as noRange.

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Subst Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Range Source #

Sized TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

ToJSON Range Source # 
Instance details

Defined in Agda.Interaction.JSONTop

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

LensClosure MetaVariable Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.Syntax.Common.Pretty

HasRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

SetRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

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) :: Type -> Type #

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

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

type SubstArg Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type Rep (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

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

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

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

Defined in Agda.Syntax.Position

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

Defined in Agda.Syntax.Position

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

Defined in Agda.Syntax.Position

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

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 :: (Foldable t, HasRange b, t b ~ a) => a -> Range Source #

Instances

Instances details
HasRange HaskellPragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pragmas

HasRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

HasRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

HasRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

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

HasRange Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Erased Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Modality Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange NotationPart Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Origin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Attribute Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

HasRange DeclarationException Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

HasRange DeclarationException' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

HasRange DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

HasRange DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

HasRange NiceDeclaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

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

HasRange ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

HasRange ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

HasRange Layer Source # 
Instance details

Defined in Agda.Syntax.Parser.Literate

Methods

getRange :: Layer -> Range Source #

HasRange ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

HasRange ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

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

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

HasRange RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

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

HasRange CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange MetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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

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

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

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Concrete

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

Defined in Agda.Syntax.Concrete

Methods

getRange :: OpApp e -> 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

HasRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

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 (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

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

Defined in Agda.Syntax.Common

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 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 :: (Functor f, SetRange b, f b ~ a) => Range -> a -> a Source #

Instances

Instances details
SetRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

SetRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

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

SetRange NotationPart Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange Attribute Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

SetRange Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

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

SetRange QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

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

SetRange ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

SetRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

SetRange AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

SetRange RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

SetRange MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

SetRange MetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

SetRange (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

Defined in Agda.Syntax.Common

Methods

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

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

SetRange (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

Defined in Agda.Syntax.Position

SetRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

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

Defined in Agda.Syntax.Position

Methods

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

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

Defined in Agda.Syntax.Position

Methods

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

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

Defined in Agda.Syntax.Common

Methods

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

class KillRange a where Source #

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

Minimal complete definition

Nothing

Methods

killRange :: KillRangeT a Source #

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

Instances

Instances details
KillRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange Suffix Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange BuiltinId Source # 
Instance details

Defined in Agda.Syntax.Builtin

KillRange PrimitiveId Source # 
Instance details

Defined in Agda.Syntax.Builtin

KillRange Access Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Erased Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange IsOpaque Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Language Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Modality Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange NameId Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange NotationPart Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange OpaqueId Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Origin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Attribute Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

KillRange Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

KillRange QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

KillRange AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange ConPatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Level Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange PatOrigin Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange PatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Substitution Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Term Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Literal Source # 
Instance details

Defined in Agda.Syntax.Literal

KillRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

KillRange RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

KillRange Compiled Source # 
Instance details

Defined in Agda.Syntax.Treeless

KillRange CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

KillRange SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

KillRange BuiltinSort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange CompiledRepresentation Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Definitions Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Projection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange ProjectionLikenessMissing Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange RewriteRuleMap Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Sections Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Signature Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange System Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

KillRange Permutation Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange Void Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange String Source #

Overlaps with KillRange [a].

Instance details

Defined in Agda.Syntax.Position

KillRange Integer Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange () Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange Bool Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange Int Source # 
Instance details

Defined in Agda.Syntax.Position

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

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Abstract

KillRange e => KillRange (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange e => KillRange (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

KillRange (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

KillRange m => KillRange (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Concrete

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

Defined in Agda.Syntax.Concrete

KillRange x => KillRange (ThingWithFixity x) Source # 
Instance details

Defined in Agda.Syntax.Fixity

KillRange t => KillRange (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

KillRange a => KillRange (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

KillRange a => KillRange (Type' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange a => KillRange (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Elim

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

Defined in Agda.Syntax.Position

KillRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange c => KillRange (Case c) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

KillRange c => KillRange (WithArity c) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

KillRange a => KillRange (SplitTree' a) Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

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

Defined in Agda.TypeChecking.Monad.Base

KillRange c => KillRange (FunctionInverse' c) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.Syntax.Position

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

Defined in Agda.Syntax.Position

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

Defined in Agda.Syntax.Position

(Ord a, KillRange a) => KillRange (Set a) Source # 
Instance details

Defined in Agda.Syntax.Position

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

Defined in Agda.Syntax.Position

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

Defined in Agda.Syntax.Position

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

Defined in Agda.Syntax.Position

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

(KillRange name, KillRange a) => KillRange (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Named name a) Source #

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Dom' t a) Source #

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

Defined in Agda.Syntax.Position

KillRange a => KillRange (Map k a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Map k a) Source #

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

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (a, b) Source #

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

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (a, b, c) Source #

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

Defined in Agda.Syntax.Common

Methods

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

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

Defined in Agda.Syntax.Position

Methods

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

type KillRangeT a = a -> a Source #

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

Remove ranges in keys and values of a map.

class KILLRANGE t b where Source #

Methods

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

Instances

Instances details
IsBase t ~ 'True => KILLRANGE t 'True Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

killRangeN :: t -> t Source #

KILLRANGE t (IsBase t) => KILLRANGE (a -> t) 'False Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

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

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

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

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

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

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 Source #

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 Source #

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)]) Source #

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.