ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Position

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

Contents

Positions
Intervals
Ranges

Synopsis

type Position
type PositionWithoutFile
data Position'
type SrcFile
data RangeFile
value mkRangeFile
value positionInvariant
value startPos
value startPos'
value movePos
value movePosByString
value backupPos
type Interval
type IntervalWithoutFile
data Interval'
value intervalInvariant
value iStart
value iEnd
value posToInterval
value getIntervalFile
value iLength
value fuseIntervals
type Range
type RangeWithoutFile
data Range'
value rangeInvariant
value consecutiveAndSeparated
value intervalsToRange
value intervalToRange
value rangeFromAbsolutePath
value rangeIntervals
value rangeFile
value rangeModule'
value rangeModule
value rightMargin
value noRange
value posToRange
value posToRange'
value rStart
value rStart'
value rEnd
value rEnd'
value rangeToInterval
value rangeToIntervalWithFile
value continuous
value continuousPerLine
newtype PrintRange
class HasRange
class HasRangeWithoutFile
class SetRange
class KillRange
type KillRangeT
value killRangeMap
class KILLRANGE
value withRangeOf
value fuseRange
value fuseRanges
value beginningOf
method beginningOfFile
value interleaveRanges

PackageAgda-2.8.0.2
Exports60
LanguageHaskell2010
LicenceMIT
SourcePosition.hs

Positions

typetype Position = Position' SrcFile

typetype PositionWithoutFile = Position' ()

datadata 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
- srcFile :: !a
  File.
- posPos :: !Word32
  Position, counting from 1.
- posLine :: !Word32
  Line number, counting from 1.
- posCol :: !Word32
  Column number, counting from 1.

Instances16Functor, Foldable, Traversable, NFData, Eq, Ord, …

Functor Position'Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Foldable Position'Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Traversable Position'Defined in Agda-2.8.0.2 · Agda.Syntax.Position
NFData PositionDefined in Agda-2.8.0.2 · Agda.Syntax.Position
NFData PositionWithoutFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
Pretty PositionWithoutFileDefined in Agda-2.8.0.2 · Agda.Syntax.Common.Pretty
Eq a => Eq (Position' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Ord a => Ord (Position' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Read a => Read (Position' a)Defined in Agda-2.8.0.2 · Agda.Interaction.Base · orphan
Show a => Show (Position' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Generic (Position' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
ToJSON (Position' ())Defined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
Pretty a => Pretty (Position' (Maybe a))Defined in Agda-2.8.0.2 · Agda.Syntax.Common.Pretty
EncodeTCM (Position' ())Defined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
EmbPrj a => EmbPrj (Position' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep (Position' a) = D1 ('MetaData "Position'" "Agda.Syntax.Position" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "Pn" 'PrefixI 'True) ((S1 ('MetaSel ('Just "srcFile") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a) :*: S1 ('MetaSel ('Just "posPos") 'NoSourceUnpackedness 'SourceStrict 'DecidedUnpack) (Rec0 Word32)) :*: (S1 ('MetaSel ('Just "posLine") 'NoSourceUnpackedness 'SourceStrict 'DecidedUnpack) (Rec0 Word32) :*: S1 ('MetaSel ('Just "posCol") 'NoSourceUnpackedness 'SourceStrict 'DecidedUnpack) (Rec0 Word32))))Defined in Agda-2.8.0.2 · Agda.Syntax.Position

typetype SrcFile = Maybe RangeFile

datadata RangeFile

Source#

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

Constructors

RangeFile
- 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.

Instances35Eq, Ord, Read, Show, Generic, NFData, …

Eq RangeFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
Only the rangeFileName component is compared.
Ord RangeFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
Only the rangeFileName component is compared.
Read RangeFileDefined in Agda-2.8.0.2 · Agda.Interaction.Base · orphan
This instance fills in the TopLevelModuleNames using Nothing. Note that these occurrences of Nothing are "overwritten" by parseIOTCM.
Show RangeFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
Generic RangeFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
NFData IntervalDefined in Agda-2.8.0.2 · Agda.Syntax.Position
NFData PositionDefined in Agda-2.8.0.2 · Agda.Syntax.Position
NFData RangeFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
ToJSON RangeDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
Pretty RangeFileDefined in Agda-2.8.0.2 · Agda.Syntax.Common.Pretty
Pretty TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleName · orphan
FreshName RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
Sized TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleName · orphan
HasRange IntervalDefined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRange RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
Subst RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
PrettyTCM RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
BeginningOfFile RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
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.
BeginningOfFile RangeFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
BeginningOfFile SrcFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
EncodeTCM RangeDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
KillRange RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
SetRange RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
EmbPrj RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Ranges are always deserialised as noRange.
EmbPrj RangeFileDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
EmbPrj TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
LensClosure MetaInfo RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensClosure MetaVariable RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasRange (TopLevelModuleName' Range)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange (TopLevelModuleName' Range)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
SetRange (TopLevelModuleName' Range)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
FreshName (Range, String)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
type Rep RangeFile = D1 ('MetaData "RangeFile" "Agda.Syntax.Position" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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)))))Defined in Agda-2.8.0.2 · Agda.Syntax.Position
type SubstArg Range = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan

valuemkRangeFile

Source#

A smart constructor for RangeFile.

valuepositionInvariant :: Position' a -> Bool

valuestartPos :: Maybe RangeFile -> Position

Source#

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

valuestartPos' :: a -> Position' a

Source#

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

valuemovePos :: 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.

valuemovePosByString :: Foldable t => Position' a -> t Char -> Position' a

Source#

Advance the position by a string.

movePosByString = foldl' movePos

valuebackupPos :: Position' a -> Position' a

Source#

Backup the position by one character.

Precondition: The character must not be 'n'.

Intervals

typetype Interval = Interval' SrcFile

typetype IntervalWithoutFile = Interval' ()

datadata 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
- getIntervalFile :: a
- iStart' :: !PositionWithoutFile
- iEnd' :: !PositionWithoutFile

Instances16Functor, Foldable, Traversable, NFData, HasRange, HasRangeWithoutFile, …

Functor Interval'Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Foldable Interval'Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Traversable Interval'Defined in Agda-2.8.0.2 · Agda.Syntax.Position
NFData IntervalDefined in Agda-2.8.0.2 · Agda.Syntax.Position
NFData IntervalWithoutFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
Pretty IntervalWithoutFileDefined in Agda-2.8.0.2 · Agda.Syntax.Common.Pretty
HasRange IntervalDefined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRangeWithoutFile IntervalWithoutFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
Eq a => Eq (Interval' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Ord a => Ord (Interval' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Read a => Read (Interval' a)Defined in Agda-2.8.0.2 · Agda.Interaction.Base · orphan
Show a => Show (Interval' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Generic (Interval' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Pretty a => Pretty (Interval' (Maybe a))Defined in Agda-2.8.0.2 · Agda.Syntax.Common.Pretty
EmbPrj a => EmbPrj (Interval' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep (Interval' a) = D1 ('MetaData "Interval'" "Agda.Syntax.Position" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "Interval" 'PrefixI 'True) (S1 ('MetaSel ('Just "getIntervalFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Just "iStart'") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PositionWithoutFile) :*: S1 ('MetaSel ('Just "iEnd'") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PositionWithoutFile))))Defined in Agda-2.8.0.2 · Agda.Syntax.Position

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

valueiStart :: Interval' a -> Position' a

valueiEnd :: Interval' a -> Position' a

valueposToInterval

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

Source#

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

valuegetIntervalFile :: Interval' a -> a

valueiLength :: Interval' a -> Word32

Source#

The length of an interval.

valuefuseIntervals

:: IntervalWithoutFile
-> IntervalWithoutFile
-> IntervalWithoutFile

Source#

Finds the least interval which covers the arguments.

Ranges

typetype Range = Range' SrcFile

typetype RangeWithoutFile = Range' ()

datadata 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.

Instances36Functor, Foldable, Traversable, ToJSON, Sized, Subst, …

Functor Range'Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Foldable Range'Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Traversable Range'Defined in Agda-2.8.0.2 · Agda.Syntax.Position
ToJSON RangeDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
Pretty TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleName · orphan
FreshName RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
Sized TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleName · orphan
HasRange RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
Subst RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
PrettyTCM RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
BeginningOfFile RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
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.
EncodeTCM RangeDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
KillRange RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
SetRange RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRangeWithoutFile RangeWithoutFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
EmbPrj RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Ranges are always deserialised as noRange.
EmbPrj TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
LensClosure MetaInfo RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensClosure MetaVariable RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
Eq a => Eq (Range' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Ord a => Ord (Range' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Read a => Read (Range' a)Defined in Agda-2.8.0.2 · Agda.Interaction.Base · orphan
Note that the grammar implemented by this instance does not necessarily match the current representation of ranges.
Show a => Show (Range' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Generic (Range' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Eq a => Semigroup (Range' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Eq a => Monoid (Range' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
NFData a => NFData (Range' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Pretty a => Pretty (Range' (Maybe a))Defined in Agda-2.8.0.2 · Agda.Syntax.Common.Pretty
Null (Range' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRange (TopLevelModuleName' Range)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange (TopLevelModuleName' Range)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
SetRange (TopLevelModuleName' Range)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
FreshName (Range, String)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
type Rep (Range' a) = D1 ('MetaData "Range'" "Agda.Syntax.Position" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "NoRange" 'PrefixI 'False) U1 :+: C1 ('MetaCons "Range" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Seq IntervalWithoutFile))))Defined in Agda-2.8.0.2 · Agda.Syntax.Position
type SubstArg Range = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan

valuerangeInvariant :: Ord a => Range' a -> Bool

Source#

Range invariant.

valueconsecutiveAndSeparated :: 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?

valueintervalsToRange :: a -> [IntervalWithoutFile] -> Range' a

Source#

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

Precondition: consecutiveAndSeparated.

valueintervalToRange :: a -> IntervalWithoutFile -> Range' a

Source#

Converts a file name and an interval to a range.

valuerangeFromAbsolutePath :: AbsolutePath -> Range

Source#

Range pointing to the first position in the given file.

valuerangeIntervals :: Range' a -> [IntervalWithoutFile]

Source#

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

valuerangeFile :: Range -> SrcFile

Source#

The file the range is pointing to.

valuerangeModule' :: 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.

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

Source#

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

valuerightMargin :: Range -> Range

Source#

Conflate a range to its right margin.

valuenoRange :: Range' a

Source#

Ranges between two unknown positions

valueposToRange :: Position' a -> Position' a -> Range' a

Source#

Converts two positions to a range.

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

valueposToRange' :: a -> PositionWithoutFile -> PositionWithoutFile -> Range' a

Source#

Converts a file name and two positions to a range.

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

Source#

The initial position in the range, if any.

valuerStart' :: Range' a -> Maybe PositionWithoutFile

Source#

The initial position in the range, if any.

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

Source#

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

valuerEnd' :: Range' a -> Maybe PositionWithoutFile

Source#

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

valuerangeToInterval :: Range' a -> Maybe IntervalWithoutFile

Source#

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

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

Source#

Converts a range to an interval, if possible.

valuecontinuous :: Range' a -> Range' a

Source#

Returns the shortest continuous range containing the given one.

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

Source#

Removes gaps between intervals on the same line.

newtypenewtype PrintRange a

Source#

Wrapper to indicate that range should be printed.

Constructors

PrintRange a

Instances6Eq, Ord, Pretty, HasRange, KillRange, SetRange

Eq a => Eq (PrintRange a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Ord a => Ord (PrintRange a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(Pretty a, HasRange a) => Pretty (PrintRange a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common.Pretty
HasRange a => HasRange (PrintRange a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange a => KillRange (PrintRange a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
SetRange a => SetRange (PrintRange a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position

classclass HasRange a where

Source#

Things that have a range are instances of this class.

Methods

getRange :: a -> Range

Instances136HasRange, …

HasRange HaskellPragmaDefined in Agda-2.8.0.2 · Agda.Compiler.MAlonzo.Pragmas
HasRange BindNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange DeclarationDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange LHSDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange LamBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange LetBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange RHSDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange SpineLHSDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange TypedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange WhereDeclarationsDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange AmbiguousQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
The range of an AmbiguousQName is the range of any of its disambiguations (they are the same concrete name).
HasRange ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
HasRange NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
HasRange QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
HasRange AccessDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange AnnotationDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange ErasedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange FixityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange IsInstanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange IsMacroDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange NotationPartDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange InductionDefined in Agda-2.8.0.2 · Agda.Syntax.Common · orphan
HasRange KwRangeDefined in Agda-2.8.0.2 · Agda.Syntax.Common.KeywordRange
HasRange AsNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange BinderDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange BoundNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange DeclarationDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange DoStmtDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange LHSDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange LHSCoreDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange LamBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange LamClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange ModuleApplicationDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange ModuleAssignmentDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange PragmaDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange RHSDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange RecordDirectiveDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange TypedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange WhereClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange AttrDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Attribute
HasRange AttributeDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Attribute
HasRange DeclarationExceptionDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Errors
HasRange DeclarationException'Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Errors
HasRange DeclarationWarningDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Errors
HasRange DeclarationWarning'Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Errors
HasRange NiceDeclarationDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Types
HasRange NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
HasRange QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
HasRange AppInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange ConPatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange DeclInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange ExprInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange LHSInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange LetInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange MetaInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange ModuleInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange MutualInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange PatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange ClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
HasRange ConHeadDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
HasRange ParseErrorDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Monad
HasRange ParseWarningDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Monad
HasRange TokenDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Tokens
HasRange IntervalDefined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRange RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRange AbstractNameDefined in Agda-2.8.0.2 · Agda.Syntax.Scope.Base
HasRange RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleName
HasRange CallDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasRange CallInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasRange CompilerPragmaDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasRange ConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasRange MetaInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasRange MetaVariableDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasRange ProblemConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasRange TCErrDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasRange TCWarningDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasRange ItemDefined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity
HasRange BoolDefined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRange ()Defined in Agda-2.8.0.2 · Agda.Syntax.Position
IsExpr e => HasRange (ExprView e)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Operators.Parser
HasRange (LHSCore' e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange (Pattern' e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange (TacticAttribute' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
HasRange (TopLevelModuleName' Range)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRange a => HasRange (Binder' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange a => HasRange (Clause' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract
HasRange a => HasRange (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange a => HasRange (HasEta' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange a => HasRange (MaybePlaceholder a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange a => HasRange (RecordDirectives' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange a => HasRange (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange a => HasRange (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange a => HasRange (FieldAssignment' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange a => HasRange (PrintRange a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRange a => HasRange (MaybeSection a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
HasRange a => HasRange (Closure a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasRange a => HasRange (List1 a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Precondition: The ranges of the list elements must point to the same file (or be empty).
HasRange a => HasRange (List2 a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRange a => HasRange (Set1 a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRange a => HasRange (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRange a => HasRange [a]Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Precondition: The ranges of the list elements must point to the same file (or be empty).
HasRange e => HasRange (OpApp e)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange a => HasRange (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange a => HasRange (Dom' t a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
(HasRange a, HasRange b) => HasRange (ImportDirective' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(HasRange a, HasRange b) => HasRange (ImportedName' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(HasRange a, HasRange b) => HasRange (Renaming' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(HasRange a, HasRange b) => HasRange (Using' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(HasRange a, HasRange b) => HasRange (Either a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(HasRange a, HasRange b) => HasRange (a, b)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Precondition: The ranges of the tuple elements must point to the same file (or be empty).
(HasRange a, HasRange b, HasRange c) => HasRange (a, b, c)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Precondition: The ranges of the tuple elements must point to the same file (or be empty).
(HasRange a, HasRange b, HasRange c, HasRange d) => HasRange (a, b, c, d)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Precondition: The ranges of the tuple elements must point to the same file (or be empty).
(HasRange qn, HasRange nm, HasRange p, HasRange e) => HasRange (RewriteEqn' qn nm p e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e) => HasRange (a, b, c, d, e)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Precondition: The ranges of the tuple elements must point to the same file (or be empty).
(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f) => HasRange (a, b, c, d, e, f)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Precondition: The ranges of the tuple elements must point to the same file (or be empty).
(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f, HasRange g) => HasRange (a, b, c, d, e, f, g)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Precondition: The ranges of the tuple elements must point to the same file (or be empty).

classclass HasRangeWithoutFile a where

Source#

Things that have a RangeWithoutFile are instances of this class.

Methods

getRangeWithoutFile :: a -> RangeWithoutFile

Instances18HasRangeWithoutFile, …

HasRangeWithoutFile LayerDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Literate
HasRangeWithoutFile TokenDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Tokens
HasRangeWithoutFile IntervalWithoutFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRangeWithoutFile RangeWithoutFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRangeWithoutFile BoolDefined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRangeWithoutFile ()Defined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRangeWithoutFile a => HasRangeWithoutFile (List1 a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRangeWithoutFile a => HasRangeWithoutFile (List2 a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRangeWithoutFile a => HasRangeWithoutFile (Set1 a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRangeWithoutFile a => HasRangeWithoutFile (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRangeWithoutFile a => HasRangeWithoutFile [a]Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(HasRangeWithoutFile a, HasRangeWithoutFile b) => HasRangeWithoutFile (Either a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(HasRangeWithoutFile a, HasRangeWithoutFile b) => HasRangeWithoutFile (a, b)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c) => HasRangeWithoutFile (a, b, c)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d) => HasRangeWithoutFile (a, b, c, d)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d, HasRangeWithoutFile e) => HasRangeWithoutFile (a, b, c, d, e)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d, HasRangeWithoutFile e, HasRangeWithoutFile f) => HasRangeWithoutFile (a, b, c, d, e, f)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d, HasRangeWithoutFile e, HasRangeWithoutFile f, HasRangeWithoutFile g) => HasRangeWithoutFile (a, b, c, d, e, f, g)Defined in Agda-2.8.0.2 · Agda.Syntax.Position

classclass 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.

Methods

setRange :: Range -> a -> a

Instances41SetRange, …

SetRange BindNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
SetRange ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
SetRange NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
SetRange QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
SetRange CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange NotationPartDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
SetRange TypedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
SetRange AttrDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Attribute
SetRange AttributeDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Attribute
SetRange NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
SetRange QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
SetRange ConPatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
SetRange DeclInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
SetRange ModuleInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
SetRange PatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
SetRange ConHeadDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
SetRange RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
SetRange AbstractNameDefined in Agda-2.8.0.2 · Agda.Syntax.Scope.Base
SetRange RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleName
SetRange MetaInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
SetRange MetaVariableDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
SetRange (Pattern' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract
SetRange (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
SetRange (TopLevelModuleName' Range)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
SetRange a => SetRange (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange a => SetRange (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange a => SetRange (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange a => SetRange (PrintRange a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
SetRange a => SetRange (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
SetRange a => SetRange [a]Defined in Agda-2.8.0.2 · Agda.Syntax.Position
SetRange a => SetRange (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

classclass KillRange a where

Source#

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

Methods

killRange :: KillRangeT a

Instances207KillRange, …

KillRange BindNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange DataDefParamsDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange DeclarationDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange GeneralizeTelescopeDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange LHSDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange LamBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange LetBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange ModuleApplicationDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange ProblemEqDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange RHSDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange RecordConNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange ScopeCopyInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange SpineLHSDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange TypedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange TypedBindingInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange WhereDeclarationsDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange AmbiguousQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
KillRange ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
KillRange NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
KillRange QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
KillRange SuffixDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract · orphan
KillRange BuiltinIdDefined in Agda-2.8.0.2 · Agda.Syntax.Builtin
KillRange PrimitiveIdDefined in Agda-2.8.0.2 · Agda.Syntax.Builtin
KillRange AccessDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange AnnotationDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange BinderNameOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange CatchallDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange ConOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange CoverageCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange ErasedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange ExpandedEllipsisDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange FixityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange Fixity'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange FreeVariablesDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange InteractionIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange IsInstanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange IsMacroDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange IsOpaqueDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange LanguageDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange NameIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange NotationPartDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange OpaqueIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange OverlapModeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange PositivityCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange ProjOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange UniverseCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange InductionDefined in Agda-2.8.0.2 · Agda.Syntax.Common · orphan
KillRange KwRangeDefined in Agda-2.8.0.2 · Agda.Syntax.Common.KeywordRange
KillRange AsNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange BinderDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange BoundNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange DeclarationDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange DoStmtDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange LHSDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange LamBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange LamClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange ModuleApplicationDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange ModuleAssignmentDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange PragmaDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange RHSDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange RecordDirectiveDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange TypedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange WhereClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange AttrDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Attribute
KillRange AttributeDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Attribute
KillRange NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
KillRange QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
KillRange AppInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange ConPatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange DeclInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange ExprInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange LHSInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange LetInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange MetaInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange ModuleInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange MutualInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange PatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange ClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange ConHeadDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange ConPatternInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange DBPatVarDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange DataOrRecordDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange LevelDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange PatOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange PatternInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange PlusLevelDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange SortDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange SubstitutionDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange TermDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange LiteralDefined in Agda-2.8.0.2 · Agda.Syntax.Literal
KillRange RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange ScopeInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Scope.Base
KillRange RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleName
KillRange CompiledDefined in Agda-2.8.0.2 · Agda.Syntax.Treeless
KillRange CompiledClausesDefined in Agda-2.8.0.2 · Agda.TypeChecking.CompiledClause
KillRange SplitTagDefined in Agda-2.8.0.2 · Agda.TypeChecking.Coverage.SplitTree
KillRange BuiltinSortDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange CompKitDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange CompiledRepresentationDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange DefinitionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange DefinitionsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange DefnDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange DisplayFormDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange DisplayTermDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange DoGeneralizeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange EtaEqualityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange ExtLamInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange FunctionFlagDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange InstanceInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange InstanceTableDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange IsForcedDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange MutualIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange NLPSortDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange NLPTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange NLPatDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange NumGeneralizableArgsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange ProjLamsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange ProjectionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange ProjectionLikenessMissingDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange RewriteRuleDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange RewriteRuleMapDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange SectionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange SectionsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange SignatureDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange SystemDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange TermHeadDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange PolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphan
KillRange OccurrenceDefined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity.Occurrence
KillRange PermutationDefined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange StringDefined in Agda-2.8.0.2 · Agda.Syntax.Position
Overlaps with KillRange [a].
KillRange VoidDefined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange IntegerDefined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange BoolDefined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange IntDefined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange ()Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange (TacticAttribute' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange (TopLevelModuleName' Range)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange (SmallSet FunctionFlag)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange a => KillRange (Binder' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange a => KillRange (Clause' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange a => KillRange (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange a => KillRange (HasEta' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange a => KillRange (MaybePlaceholder a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange a => KillRange (RecordDirectives' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange a => KillRange (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange a => KillRange (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange a => KillRange (FieldAssignment' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange a => KillRange (Abs a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange a => KillRange (Blocked a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange a => KillRange (Pattern' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange a => KillRange (Tele a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange a => KillRange (Type' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
KillRange a => KillRange (Elim' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Elim
KillRange a => KillRange (PrintRange a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange a => KillRange (SplitTree' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Coverage.SplitTree
KillRange a => KillRange (Closure a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange a => KillRange (Open a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange a => KillRange (List1 a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange a => KillRange (List2 a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange a => KillRange (Drop a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange a => KillRange (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange a => KillRange (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange a => KillRange [a]Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange c => KillRange (Case c)Defined in Agda-2.8.0.2 · Agda.TypeChecking.CompiledClause
KillRange c => KillRange (WithArity c)Defined in Agda-2.8.0.2 · Agda.TypeChecking.CompiledClause
KillRange c => KillRange (FunctionInverse' c)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange e => KillRange (LHSCore' e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange e => KillRange (Pattern' e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange e => KillRange (OpApp e)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange m => KillRange (TerminationCheck m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange t => KillRange (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
KillRange x => KillRange (ThingWithFixity x)Defined in Agda-2.8.0.2 · Agda.Syntax.Fixity
(KillRange a, Ord a) => KillRange (DiscrimTree a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.DiscrimTree.Types
(Ord a, KillRange a) => KillRange (Set1 a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(Ord a, KillRange a) => KillRange (Set a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange a => KillRange (Map k a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(KillRange a, KillRange b) => KillRange (ImportDirective' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(KillRange a, KillRange b) => KillRange (ImportedName' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(KillRange a, KillRange b) => KillRange (Renaming' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(KillRange a, KillRange b) => KillRange (Using' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(KillRange a, KillRange b) => KillRange (Either a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(KillRange a, KillRange b) => KillRange (a, b)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(KillRange name, KillRange a) => KillRange (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(KillRange t, KillRange a) => KillRange (Dom' t a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
(KillRange a, KillRange b, KillRange c) => KillRange (a, b, c)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(KillRange a, KillRange b, KillRange c, KillRange d) => KillRange (a, b, c, d)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
(KillRange qn, KillRange nm, KillRange e, KillRange p) => KillRange (RewriteEqn' qn nm p e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

typetype KillRangeT a = a -> a

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

Source#

Remove ranges in keys and values of a map.

classclass KILLRANGE t (b :: Bool) where

Methods

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

Instances2KILLRANGE

IsBase t ~ 'True => KILLRANGE t 'TrueDefined in Agda-2.8.0.2 · Agda.Syntax.Position
KILLRANGE t (IsBase t) => KILLRANGE (a -> t) 'FalseDefined in Agda-2.8.0.2 · Agda.Syntax.Position

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

Source#

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

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

Source#

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

valuefuseRanges :: 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).

valuebeginningOf :: 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.

methodbeginningOfFile :: a -> Range

Source#

Return an empty range (a single, empty interval) at the beginning of the file.

valueinterleaveRanges :: HasRangeWithoutFile 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.