Agda-2.3.0: A dependently typed functional programming language and proof assistant

Agda.Syntax.Position

Contents

Description

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

Synopsis

Positions

data Position

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

srcFile :: Maybe AbsolutePath

File.

posPos :: !Int32

Position.

posLine :: !Int32

Line number, counting from 1.

posCol :: !Int32

Column number, counting from 1.

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 

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] 

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

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

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

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

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

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

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

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

killRange7 :: (KillRange a1, KillRange a2, KillRange a3, KillRange a6, KillRange a4, KillRange a5, KillRange a) => (a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> 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

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

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

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.

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

Tests

tests :: IO Bool

Test suite.