HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Position

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

  • 12 types
  • 4 classes
  • 40 values
  • PackageAgda-2.7.0.1
  • Exports56
  • LanguageHaskell2010
  • LicenceMIT
  • SourcePosition.hs

Positions

12 declarations
datadata Position' a
#

Represents a point in the input.

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

Note the invariant which positions have to satisfy: positionInvariant.

Constructors

Instances16Functor, Foldable, Traversable, NFData, Eq, Ord, …
datadata RangeFile
#

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.

Instances32Eq, Ord, Read, Show, Generic, NFData, …
valuemovePos :: Position' a -> Char -> Position' a
#

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

valuestartPos' :: a -> Position' a
#

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

Intervals

9 declarations
datadata Interval' a
#

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

Note the invariant which intervals have to satisfy: intervalInvariant.

Constructors

Instances15Functor, Foldable, Traversable, NFData, HasRange, Eq, …

Ranges

35 declarations
datadata Range' a
#

A range is a file name, plus a sequence of intervals, assumed to point to the given file. The intervals should be consecutive and separated.

Note the invariant which ranges have to satisfy: rangeInvariant.

Constructors

Instances34Functor, Foldable, Traversable, ToJSON, Subst, PrettyTCM, …
newtypenewtype PrintRange a
#

Wrapper to indicate that range should be printed.

Constructors

Instances6Eq, Ord, Pretty, HasRange, KillRange, SetRange
classclass HasRange a where
#

Things that have a range are instances of this class.

Methods

Instances131HasRange, …
classclass HasRange a => SetRange a where
#

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

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

Methods

Instances37SetRange, …
classclass KillRange a where
#

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

Methods

Instances198KillRange, …
valuefuseRanges :: Ord a => Range' a -> Range' a -> Range' a
#

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

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

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

valuebeginningOf :: Range -> Range
#

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

valuebeginningOfFile :: Range -> Range
#

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

valueinterleaveRanges :: HasRange a => [a] -> [a] -> ([a], [(a, a)])
#

Interleaves two streams of ranged elements

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