Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda.Syntax.Position
Description
Position information for syntax. Crucial for giving good error messages.
- type Position = Position' SrcFile
- data Position' a = Pn {}
- positionInvariant :: Position' a -> Bool
- startPos :: Maybe AbsolutePath -> Position
- movePos :: Position' a -> Char -> Position' a
- movePosByString :: Position' a -> String -> Position' a
- backupPos :: Position' a -> Position' a
- type Interval = Interval' SrcFile
- data Interval' a = Interval {}
- intervalInvariant :: Ord a => Interval' a -> Bool
- takeI :: String -> Interval' a -> Interval' a
- dropI :: String -> Interval' a -> Interval' a
- type Range = Range' SrcFile
- newtype Range' a = Range [Interval' a]
- rangeInvariant :: Range -> Bool
- rightMargin :: Range -> Range
- noRange :: Range' a
- posToRange :: Ord a => Position' a -> Position' a -> Range' a
- rStart :: Range' a -> Maybe (Position' a)
- rEnd :: Range' a -> Maybe (Position' a)
- rangeToInterval :: Range' a -> Maybe (Interval' a)
- continuous :: Range' a -> Range' a
- continuousPerLine :: Ord a => Range' a -> Range' a
- class HasRange t where
- class HasRange t => SetRange t where
- class KillRange a where
- killRange :: KillRangeT a
- type KillRangeT a = a -> a
- killRange1 :: KillRange a => (a -> t) -> a -> t
- killRange2 :: (KillRange s, KillRange a) => (s -> a -> t) -> s -> a -> t
- killRange3 :: (KillRange s1, KillRange s, KillRange a) => (s1 -> s -> a -> t) -> s1 -> s -> a -> t
- killRange4 :: (KillRange s2, KillRange s1, KillRange s, KillRange a) => (s2 -> s1 -> s -> a -> t) -> s2 -> s1 -> s -> a -> t
- killRange5 :: (KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s3 -> s2 -> s1 -> s -> a -> t) -> s3 -> s2 -> s1 -> s -> a -> t
- killRange6 :: (KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- killRange7 :: (KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- killRange8 :: (KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- killRange9 :: (KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- killRange10 :: (KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- killRange11 :: (KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- killRange12 :: (KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- killRange13 :: (KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- killRange14 :: (KillRange s12, KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- killRange15 :: (KillRange s13, KillRange s12, KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- killRange16 :: (KillRange s14, KillRange s13, KillRange s12, KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- killRange17 :: (KillRange s15, KillRange s14, KillRange s13, KillRange s12, KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s15 -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s15 -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- killRange18 :: (KillRange s16, KillRange s15, KillRange s14, KillRange s13, KillRange s12, KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s16 -> s15 -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s16 -> s15 -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- killRange19 :: (KillRange s17, KillRange s16, KillRange s15, KillRange s14, KillRange s13, KillRange s12, KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s17 -> s16 -> s15 -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s17 -> s16 -> s15 -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
- 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
- tests :: IO Bool
Positions
data Position' a
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
Functor Position' | |
Foldable Position' | |
Traversable Position' | |
PrettyTCM Position | |
EmbPrj Position | |
Eq a => Eq (Position' a) | |
Ord a => Ord (Position' a) | |
Read a => Read (Position' a) | |
Show (Position' Integer) | |
Show a => Show (Position' (Maybe a)) | |
Arbitrary a => Arbitrary (Position' a) | |
Typeable (* -> *) Position' |
positionInvariant :: Position' a -> Bool
startPos :: Maybe AbsolutePath -> Position
The first position in a file: position 1, line 1, column 1.
movePos :: Position' a -> Char -> Position' a
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' a -> String -> Position' a
Advance the position by a string.
movePosByString = foldl' movePos
backupPos :: Position' a -> Position' a
Backup the position by one character.
Precondition: The character must not be '\n'
.
Intervals
data Interval' a
An interval. The iEnd
position is not included in the interval.
Note the invariant which intervals have to satisfy: intervalInvariant
.
Instances
Functor Interval' | |
Foldable Interval' | |
Traversable Interval' | |
HasRange Interval | |
PrettyTCM Interval | |
EmbPrj Interval | |
Eq a => Eq (Interval' a) | |
Ord a => Ord (Interval' a) | |
Read a => Read (Interval' a) | |
Show (Interval' Integer) | |
Show a => Show (Interval' (Maybe a)) | |
(Arbitrary a, Ord a) => Arbitrary (Interval' a) | |
Typeable (* -> *) Interval' |
intervalInvariant :: Ord a => Interval' a -> Bool
takeI :: String -> Interval' a -> Interval' a
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' a -> Interval' a
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
A range is a list of intervals. The intervals should be consecutive and separated.
Note the invariant which ranges have to satisfy: rangeInvariant
.
Instances
Functor Range' | |
Foldable Range' | |
Traversable Range' | |
KillRange Range | |
SetRange Range | |
HasRange Range | |
FreshName Range | |
GenC Range | |
PrettyTCM Range | |
EmbPrj Range | |
Eq a => Eq (Range' a) | |
Ord a => Ord (Range' a) | |
Read a => Read (Range' a) | |
Show (Range' Integer) | |
Show a => Show (Range' (Maybe a)) | |
(Ord a, Arbitrary a) => Arbitrary (Range' a) | |
FreshName (Range, String) | |
Typeable (* -> *) Range' |
rangeInvariant :: Range -> Bool
rightMargin :: Range -> Range
Conflate a range to its right margin.
posToRange :: Ord a => Position' a -> Position' a -> Range' a
Converts two positions to a range.
rangeToInterval :: Range' a -> Maybe (Interval' a)
Converts a range to an interval, if possible.
continuous :: Range' a -> Range' a
Returns the shortest continuous range containing the given one.
continuousPerLine :: Ord a => Range' a -> Range' a
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 :: KillRangeT a
Instances
type KillRangeT a = a -> a
killRange1 :: KillRange a => (a -> t) -> a -> t
killRange2 :: (KillRange s, KillRange a) => (s -> a -> t) -> s -> a -> t
killRange3 :: (KillRange s1, KillRange s, KillRange a) => (s1 -> s -> a -> t) -> s1 -> s -> a -> t
killRange4 :: (KillRange s2, KillRange s1, KillRange s, KillRange a) => (s2 -> s1 -> s -> a -> t) -> s2 -> s1 -> s -> a -> t
killRange5 :: (KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s3 -> s2 -> s1 -> s -> a -> t) -> s3 -> s2 -> s1 -> s -> a -> t
killRange6 :: (KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
killRange7 :: (KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
killRange8 :: (KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
killRange9 :: (KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
killRange10 :: (KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
killRange11 :: (KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
killRange12 :: (KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
killRange13 :: (KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
killRange14 :: (KillRange s12, KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
killRange15 :: (KillRange s13, KillRange s12, KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
killRange16 :: (KillRange s14, KillRange s13, KillRange s12, KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
killRange17 :: (KillRange s15, KillRange s14, KillRange s13, KillRange s12, KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s15 -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s15 -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
killRange18 :: (KillRange s16, KillRange s15, KillRange s14, KillRange s13, KillRange s12, KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s16 -> s15 -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s16 -> s15 -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
killRange19 :: (KillRange s17, KillRange s16, KillRange s15, KillRange s14, KillRange s13, KillRange s12, KillRange s11, KillRange s10, KillRange s9, KillRange s8, KillRange s7, KillRange s6, KillRange s5, KillRange s4, KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s17 -> s16 -> s15 -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t) -> s17 -> s16 -> s15 -> s14 -> s13 -> s12 -> s11 -> s10 -> s9 -> s8 -> s7 -> s6 -> s5 -> s4 -> s3 -> s2 -> s1 -> s -> a -> t
withRangeOf :: (SetRange t, HasRange u) => t -> u -> t
x `withRangeOf` y
sets the range of x
to the range of y
.
fuseRanges :: Ord a => Range' a -> Range' a -> Range' a
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.