Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 :: !Int32
posLine :: !Int32
posCol :: !Int32
}
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 :: 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
fuseRange :: (HasRange u, HasRange t) => u -> t -> Range
fuseRanges :: Range -> Range -> Range
beginningOf :: Range -> Range
beginningOfFile :: Range -> Range
tests :: IO Bool
Positions
data Position 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 :: Maybe AbsolutePathFile.
posPos :: !Int32Position.
posLine :: !Int32Line number, counting from 1.
posCol :: !Int32Column number, counting from 1.
positionInvariant :: Position -> BoolSource
startPos :: Maybe AbsolutePath -> PositionSource
The first position in a file: position 1, line 1, column 1.
movePos :: Position -> Char -> PositionSource
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 -> PositionSource

Advance the position by a string.

 movePosByString = foldl' movePos
backupPos :: Position -> PositionSource

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
intervalInvariant :: Interval -> BoolSource
takeI :: String -> Interval -> IntervalSource

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

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]
rangeInvariant :: Range -> BoolSource
noRange :: RangeSource
Ranges between two unknown positions
posToRange :: Position -> Position -> RangeSource
Converts two positions to a range.
rStart :: Range -> Maybe PositionSource
The initial position in the range, if any.
rEnd :: Range -> Maybe PositionSource
The position after the final position in the range, if any.
rangeToInterval :: Range -> Maybe IntervalSource
Converts a range to an interval, if possible.
continuous :: Range -> RangeSource
Returns the shortest continuous range containing the given one.
continuousPerLine :: Range -> RangeSource
Removes gaps between intervals on the same line.
class HasRange t whereSource
Things that have a range are instances of this class.
Methods
getRange :: t -> RangeSource
class HasRange t => SetRange t whereSource

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 -> tSource
class KillRange a whereSource
Killing the range of an object sets all range information to noRange.
Methods
killRange :: a -> aSource
killRange1 :: KillRange a => (a -> t) -> a -> tSource
killRange2 :: (KillRange a, KillRange a1) => (a -> a1 -> t) -> a -> a1 -> tSource
killRange3 :: (KillRange a, KillRange a1, KillRange a2) => (a -> a1 -> a2 -> t) -> a -> a1 -> a2 -> tSource
killRange4 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3) => (a -> a1 -> a2 -> a3 -> t) -> a -> a1 -> a2 -> a3 -> tSource
killRange5 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4) => (a -> a1 -> a2 -> a3 -> a4 -> t) -> a -> a1 -> a2 -> a3 -> a4 -> tSource
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 -> tSource
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 -> tSource
withRangeOf :: (SetRange t, HasRange u) => t -> u -> tSource
x withRangeOf y sets the range of x to the range of y.
fuseRange :: (HasRange u, HasRange t) => u -> t -> RangeSource
fuseRanges :: Range -> Range -> RangeSource
Finds a range which covers the arguments.
beginningOf :: Range -> RangeSource
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 -> RangeSource
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 BoolSource
Test suite.
Produced by Haddock version 2.6.1