| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Syntax.Position

Contents

Positions
Intervals
Ranges
Tests

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

data Position = Pn {

srcFile :: Maybe AbsolutePath
posPos :: !Int
posLine :: !Int
posCol :: !Int

}

positionInvariant :: Position -> Bool
startPos :: Maybe AbsolutePath -> Position
movePos :: Position -> Char -> Position
movePosByString :: Position -> String -> Position
backupPos :: Position -> Position

data Interval = Interval {

iStart :: !Position
iEnd :: !Position

}

intervalInvariant :: Interval -> Bool
takeI :: String -> Interval -> Interval
dropI :: String -> Interval -> Interval
newtype Range = Range [Interval]
rangeInvariant :: Range -> Bool
noRange :: Range
posToRange :: Position -> Position -> Range
rStart :: Range -> Maybe Position
rEnd :: Range -> Maybe Position
rangeToInterval :: Range -> Maybe Interval
continuous :: Range -> Range
continuousPerLine :: Range -> Range
class HasRange t where

getRange :: t -> Range

class HasRange t => SetRange t where

setRange :: Range -> t -> t

class KillRange a where

killRange :: a -> a

killRange1
killRange2
killRange3
killRange4
killRange5
killRange6
killRange7
withRangeOf :: (SetRange t, HasRange u) => t -> u -> t
fuseRange :: (HasRange u, HasRange t) => u -> t -> Range
fuseRanges :: Range -> Range -> Range
beginningOf :: Range -> Range
tests :: IO Bool

Positions

data Position | Source

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 |

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

startPos :: Maybe AbsolutePath -> Position | Source

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

movePos :: Position -> Char -> Position | 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 :: Position -> String -> Position | Source

Advance the position by a string.

     movePosByString = foldl' movePos

backupPos :: Position -> Position | Source

Backup the position by one character. Precondition: The character must not be `'\n'`.
Intervals

data Interval | Source

An interval. The `iEnd` position is not included in the interval. Note the invariant which intervals have to satisfy: `intervalInvariant`.
Constructors

Interval |

iStart :: !Position |
iEnd :: !Position |

Instances

Eq Interval
Data Interval
Ord Interval
Show Interval
Typeable Interval
Arbitrary Interval
HasRange Interval
EmbPrj Interval

intervalInvariant :: Interval -> Bool | Source

takeI :: String -> Interval -> Interval | Source

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

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

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
EmbPrj Range
GenC Range

rangeInvariant :: Range -> Bool | Source

noRange :: Range | Source

Ranges between two unknown positions

posToRange :: Position -> Position -> Range | Source

Converts two positions to a range.

rStart :: Range -> Maybe Position | Source

The initial position in the range, if any.

rEnd :: Range -> Maybe Position | Source

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

rangeToInterval :: Range -> Maybe Interval | Source

Converts a range to an interval, if possible.

continuous :: Range -> Range | Source

Returns the shortest continuous range containing the given one.

continuousPerLine :: Range -> Range | Source

Removes gaps between intervals on the same line.

class HasRange t where | Source

Things that have a range are instances of this class.
Methods

getRange :: t -> Range | Source

Instances

HasRange Range
HasRange Interval
HasRange ParseError
HasRange Literal
HasRange QName
HasRange Name
HasRange Token
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 DeclarationException
HasRange NiceDefinition
HasRange NiceDeclaration
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 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 | 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 -> t -> t | Source

Instances

SetRange Range
SetRange Literal
SetRange Name
SetRange ModuleName
SetRange QName
SetRange Name
SetRange AbstractName
SetRange MetaVariable

class KillRange a where | Source

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

killRange :: a -> a | Source

Instances

KillRange Range
KillRange Literal
KillRange Hiding
KillRange Induction
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
killRange2
killRange3
killRange4
killRange5
killRange6
killRange7

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

fuseRanges :: Range -> Range -> Range | Source

Finds a range which covers the arguments.

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

tests :: IO Bool | Source

Test suite.
Produced by Haddock version 2.4.2