| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Position
Description
Position information for syntax. Crucial for giving good error messages.
Synopsis
- type Position = Position' SrcFile
- type PositionWithoutFile = Position' ()
- data Position' a = Pn {}
- type SrcFile = Maybe RangeFile
- data RangeFile = RangeFile {}
- mkRangeFile :: AbsolutePath -> Maybe (TopLevelModuleName' Range) -> RangeFile
- positionInvariant :: Position' a -> Bool
- startPos :: Maybe RangeFile -> Position
- movePos :: Position' a -> Char -> Position' a
- movePosByString :: Foldable t => Position' a -> t Char -> Position' a
- backupPos :: Position' a -> Position' a
- startPos' :: a -> Position' a
- type Interval = Interval' SrcFile
- type IntervalWithoutFile = Interval' ()
- data Interval' a = Interval {}
- intervalInvariant :: Ord a => Interval' a -> Bool
- posToInterval :: a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
- getIntervalFile :: Interval' a -> a
- iLength :: Interval' a -> Int32
- fuseIntervals :: Ord a => Interval' a -> Interval' a -> Interval' a
- setIntervalFile :: a -> Interval' b -> Interval' a
- type Range = Range' SrcFile
- data Range' a
- = NoRange
- | Range !a (Seq IntervalWithoutFile)
- rangeInvariant :: Ord a => Range' a -> Bool
- consecutiveAndSeparated :: Ord a => [Interval' a] -> Bool
- intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a
- intervalToRange :: a -> IntervalWithoutFile -> Range' a
- rangeIntervals :: Range' a -> [IntervalWithoutFile]
- rangeFile :: Range -> SrcFile
- rangeModule' :: Range -> Maybe (Maybe (TopLevelModuleName' Range))
- rangeModule :: Range -> Maybe (TopLevelModuleName' Range)
- rightMargin :: Range -> Range
- noRange :: Range' a
- posToRange :: Position' a -> Position' a -> Range' a
- posToRange' :: a -> PositionWithoutFile -> PositionWithoutFile -> Range' a
- rStart :: Range' a -> Maybe (Position' a)
- rStart' :: Range' a -> Maybe PositionWithoutFile
- rEnd :: Range' a -> Maybe (Position' a)
- rEnd' :: Range' a -> Maybe PositionWithoutFile
- rangeToInterval :: Range' a -> Maybe IntervalWithoutFile
- rangeToIntervalWithFile :: Range' a -> Maybe (Interval' a)
- continuous :: Range' a -> Range' a
- continuousPerLine :: Ord a => Range' a -> Range' a
- newtype PrintRange a = PrintRange a
- class HasRange a where
- class HasRange a => SetRange a where
- class KillRange a where
- killRange :: KillRangeT a
- type KillRangeT a = a -> a
- killRangeMap :: (KillRange k, KillRange v) => KillRangeT (Map k v)
- class KILLRANGE t b where
- withRangeOf :: (SetRange t, HasRange u) => t -> u -> t
- fuseRange :: (HasRange u, HasRange t) => u -> t -> Range
- fuseRanges :: Ord a => Range' a -> Range' a -> Range' a
- beginningOf :: Range -> Range
- beginningOfFile :: Range -> Range
- interleaveRanges :: HasRange a => [a] -> [a] -> ([a], [(a, a)])
Positions
type PositionWithoutFile = 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 | |
Instances
Constructors
| RangeFile | |
Fields
| |
Instances
mkRangeFile :: AbsolutePath -> Maybe (TopLevelModuleName' Range) -> RangeFile Source #
A smart constructor for RangeFile.
positionInvariant :: Position' a -> Bool Source #
startPos :: Maybe RangeFile -> Position Source #
The first position in a file: position 1, line 1, column 1.
movePos :: Position' a -> Char -> Position' a 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 :: Foldable t => Position' a -> t Char -> Position' a Source #
Advance the position by a string.
movePosByString = foldl' movePos
backupPos :: Position' a -> Position' a Source #
Backup the position by one character.
Precondition: The character must not be 'n'.
Intervals
type IntervalWithoutFile = Interval' () Source #
An interval. The iEnd position is not included in the interval.
Note the invariant which intervals have to satisfy: intervalInvariant.
Instances
posToInterval :: a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a Source #
Converts a file name and two positions to an interval.
getIntervalFile :: Interval' a -> a Source #
Gets the srcFile component of the interval. Because of the invariant,
they are both the same.
fuseIntervals :: Ord a => Interval' a -> Interval' a -> Interval' a Source #
Finds the least interval which covers the arguments.
Precondition: The intervals must point to the same file.
setIntervalFile :: a -> Interval' b -> Interval' a Source #
Sets the srcFile components of the interval.
Ranges
A range is a file name, plus a sequence of intervals, assumed to point to the given file. The intervals should be consecutive and separated.
Note the invariant which ranges have to satisfy: rangeInvariant.
Constructors
| NoRange | |
| Range !a (Seq IntervalWithoutFile) |
Instances
consecutiveAndSeparated :: Ord a => [Interval' a] -> Bool Source #
Are the intervals consecutive and separated, do they all point to the same file, and do they satisfy the interval invariant?
intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a Source #
Turns a file name plus a list of intervals into a range.
Precondition: consecutiveAndSeparated.
intervalToRange :: a -> IntervalWithoutFile -> Range' a Source #
Converts a file name and an interval to a range.
rangeIntervals :: Range' a -> [IntervalWithoutFile] Source #
The intervals that make up the range. The intervals are
consecutive and separated (consecutiveAndSeparated).
rangeModule' :: Range -> Maybe (Maybe (TopLevelModuleName' Range)) Source #
rangeModule :: Range -> Maybe (TopLevelModuleName' Range) Source #
The range's top-level module name, if any.
rightMargin :: Range -> Range Source #
Conflate a range to its right margin.
posToRange :: Position' a -> Position' a -> Range' a Source #
Converts two positions to a range.
Precondition: The positions have to point to the same file.
posToRange' :: a -> PositionWithoutFile -> PositionWithoutFile -> Range' a Source #
Converts a file name and two positions to a range.
rEnd :: Range' a -> Maybe (Position' a) Source #
The position after the final position in the range, if any.
rEnd' :: Range' a -> Maybe PositionWithoutFile Source #
The position after the final position in the range, if any.
rangeToInterval :: Range' a -> Maybe IntervalWithoutFile Source #
Converts a range to an interval, if possible. Note that the information about the source file is lost.
rangeToIntervalWithFile :: Range' a -> Maybe (Interval' a) Source #
Converts a range to an interval, if possible.
continuous :: Range' a -> Range' a Source #
Returns the shortest continuous range containing the given one.
continuousPerLine :: Ord a => Range' a -> Range' a Source #
Removes gaps between intervals on the same line.
newtype PrintRange a Source #
Wrapper to indicate that range should be printed.
Constructors
| PrintRange a |
Instances
class HasRange a where Source #
Things that have a range are instances of this class.
Minimal complete definition
Nothing
Methods
Instances
class HasRange a => SetRange a where Source #
If it is also possible to set the range, this is the class.
Minimal complete definition
Nothing
Methods
Instances
class KillRange a where Source #
Killing the range of an object sets all range information to noRange.
Minimal complete definition
Nothing
Methods
killRange :: KillRangeT a Source #
Instances
type KillRangeT a = a -> a Source #
killRangeMap :: (KillRange k, KillRange v) => KillRangeT (Map k v) Source #
Remove ranges in keys and values of a map.
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 #
Precondition: The ranges must point to the same file (or be empty).
fuseRanges :: Ord a => Range' a -> Range' a -> Range' a Source #
fuseRanges r r' unions the ranges r and r'.
Meaning it finds the least range r0 that covers r and r'.
Precondition: The ranges must point to the same file (or be empty).
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.
beginningOfFile :: Range -> Range Source #
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.
interleaveRanges :: HasRange a => [a] -> [a] -> ([a], [(a, a)]) Source #
Interleaves two streams of ranged elements
It will report the conflicts as a list of conflicting pairs. In case of conflict, the element with the earliest start position is placed first. In case of a tie, the element with the earliest ending position is placed first. If both tie, the element from the first list is placed first.