Agda.Syntax.Position
Description
Position information for syntax. Crucial for giving good error messages.
- data Position = Pn {}
- positionInvariant :: Position -> Bool
- startPos :: Maybe AbsolutePath -> Position
- movePos :: Position -> Char -> Position
- movePosByString :: Position -> String -> Position
- backupPos :: Position -> Position
- data Interval = Interval {}
- 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
- class HasRange t => SetRange t where
- class KillRange a where
- killRange :: a -> a
- 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
- fuseRange :: (HasRange u, HasRange t) => u -> t -> Range
- fuseRanges :: Range -> Range -> Range
- beginningOf :: Range -> Range
- beginningOfFile :: Range -> Range
- tests :: IO Bool
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 | |
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
.
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
.
rangeInvariant :: Range -> Bool
posToRange :: Position -> Position -> Range
Converts two positions to a range.
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.
Instances
class KillRange a where
Killing the range of an object sets all range information to noRange
.
Methods
killRange :: a -> a
Instances
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
sets the range of withRangeOf
yx
to the range of y
.
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.