Agda.Syntax.Position

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

Positions

data Position

Represents a point in the input (file, position, line, col). Positions and line and column numbers start from 1.

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

Note the invariant which positions have to satisfy: positionInvariant.

Constructors

Pn

Fields

srcFile :: Maybe AbsolutePath

posPos :: !Int

posLine :: !Int

posCol :: !Int

Instances

Eq Position

Data Position

Ord Position

Show Position

Typeable Position

Arbitrary Position

EmbPrj Position

positionInvariant :: Position -> Bool

startPos :: Maybe AbsolutePath -> Position

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

movePos :: Position -> Char -> Position

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 :: Position -> String -> Position

Advance the position by a string.

 movePosByString = foldl' movePos

backupPos :: Position -> Position

Backup the position by one character.

Precondition: The character must not be '\n'.

Intervals

data Interval

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

Note the invariant which intervals have to satisfy: intervalInvariant.

Constructors

Interval

Fields

iStart :: !Position

iEnd :: !Position

Instances

Eq Interval

Data Interval

Ord Interval

Show Interval

Typeable Interval

Arbitrary Interval

Generates an interval located in the same file as the given interval.

HasRange Interval

EmbPrj Interval

intervalInvariant :: Interval -> Bool

takeI :: String -> Interval -> Interval

Extracts the interval corresponding to the given string, assuming that the string starts at the beginning of the given interval.

Precondition: The string must not be too long for the interval.

dropI :: String -> Interval -> Interval

Removes the interval corresponding to the given string from the given interval, assuming that the string starts at the beginning of the interval.

Precondition: The string must not be too long for the interval.

Ranges

newtype Range

A range is a list of intervals. The intervals should be consecutive and separated.

Note the invariant which ranges have to satisfy: rangeInvariant.

Constructors

Range [Interval]

Instances

Eq Range

Data Range

Ord Range

Show Range

Typeable Range

Arbitrary Range

KillRange Range

SetRange Range

HasRange Range

GenC Range

EmbPrj Range

rangeInvariant :: Range -> Bool

noRange :: Range

Ranges between two unknown positions

posToRange :: Position -> Position -> Range

Converts two positions to a range.

rStart :: Range -> Maybe Position

The initial position in the range, if any.

rEnd :: Range -> Maybe Position

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

rangeToInterval :: Range -> Maybe Interval

Converts a range to an interval, if possible.

continuous :: Range -> Range

Returns the shortest continuous range containing the given one.

continuousPerLine :: Range -> Range

Removes gaps between intervals on the same line.

class HasRange t where

Things that have a range are instances of this class.

Methods

getRange :: t -> Range

Instances

HasRange Range

HasRange Interval

HasRange Literal

HasRange QName

HasRange Name

HasRange Fixity

HasRange Pragma

HasRange Declaration

HasRange AsName

HasRange Renaming

HasRange ImportedName

HasRange UsingOrHiding

HasRange ImportDirective

HasRange WhereClause

HasRange RHS

HasRange LHS

HasRange TypedBinding

HasRange BoundName

HasRange TypedBindings

HasRange LamBinding

HasRange Pattern

HasRange Expr

HasRange AmbiguousQName

HasRange ModuleName

HasRange QName

HasRange Name

HasRange Clause

HasRange AbstractName

HasRange PatInfo

HasRange LHSInfo

HasRange DeclInfo

HasRange DefInfo

HasRange LetInfo

HasRange ModuleInfo

HasRange ExprInfo

HasRange MetaInfo

HasRange LHS

HasRange RHS

HasRange Clause

HasRange TypedBinding

HasRange TypedBindings

HasRange LamBinding

HasRange Definition

HasRange LetBinding

HasRange Declaration

HasRange Expr

HasRange Head

HasRange DeclarationException

HasRange NiceDefinition

HasRange NiceDeclaration

HasRange Token

HasRange ParseError

HasRange TCErr

HasRange TCErr'

HasRange Call

HasRange MetaVariable

HasRange a => HasRange [a]

HasRange a => HasRange (Maybe a)

HasRange a => HasRange (ParentCall a)

HasRange a => HasRange (Trace a)

HasRange a => HasRange (Arg a)

HasRange (Pattern' e)

HasRange a => HasRange (Closure a)

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

HasRange a => HasRange (Named name a)

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

class HasRange t => SetRange t where

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

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

Methods

setRange :: Range -> t -> t

Instances

SetRange Range

SetRange Literal

SetRange Name

SetRange ModuleName

SetRange QName

SetRange Name

SetRange AbstractName

SetRange MetaVariable

class KillRange a where

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

Methods

killRange :: a -> a

Instances

KillRange Range

KillRange Hiding

KillRange Induction

KillRange Literal

KillRange QName

KillRange Name

KillRange AmbiguousQName

KillRange ModuleName

KillRange QName

KillRange Name

KillRange Telescope

KillRange Sort

KillRange Type

KillRange Term

KillRange PatInfo

KillRange LHSInfo

KillRange DeclInfo

KillRange DefInfo

KillRange LetInfo

KillRange ModuleInfo

KillRange ExprInfo

KillRange MetaInfo

KillRange LHS

KillRange RHS

KillRange Clause

KillRange TypedBinding

KillRange TypedBindings

KillRange LamBinding

KillRange Definition

KillRange LetBinding

KillRange Declaration

KillRange Expr

KillRange a => KillRange [a]

KillRange a => KillRange (Maybe a)

KillRange a => KillRange (Arg a)

KillRange a => KillRange (Abs a)

KillRange a => KillRange (Blocked a)

KillRange e => KillRange (Pattern' e)

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

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

KillRange a => KillRange (Named name a)

killRange1 :: KillRange a => (a -> t) -> a -> t

killRange2 :: (KillRange a, KillRange a1) => (a -> a1 -> t) -> a -> a1 -> t

killRange3 :: (KillRange a, KillRange a1, KillRange a2) => (a -> a1 -> a2 -> t) -> a -> a1 -> a2 -> t

killRange4 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3) => (a -> a1 -> a2 -> a3 -> t) -> a -> a1 -> a2 -> a3 -> t

killRange5 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4) => (a -> a1 -> a2 -> a3 -> a4 -> t) -> a -> a1 -> a2 -> a3 -> a4 -> t

killRange6 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5) => (a -> a1 -> a2 -> a3 -> a4 -> a5 -> t) -> a -> a1 -> a2 -> a3 -> a4 -> a5 -> t

killRange7 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5, KillRange a6) => (a -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> t) -> a -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> t

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

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

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

fuseRanges :: Range -> Range -> Range

Finds a range which covers the arguments.

beginningOf :: Range -> Range

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

Tests

tests :: IO Bool

Test suite.