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
- newtype PrintRange a = PrintRange 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 -> b) -> a -> b
- killRange2 :: (KillRange a, KillRange b) => (a -> b -> c) -> a -> b -> c
- killRange3 :: (KillRange a, KillRange b, KillRange c) => (a -> b -> c -> d) -> a -> b -> c -> d
- killRange4 :: (KillRange a, KillRange b, KillRange c, KillRange d) => (a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
- killRange5 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e) => (a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
- killRange6 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f) => (a -> b -> c -> d -> e -> f -> g) -> a -> b -> c -> d -> e -> f -> g
- killRange7 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g) => (a -> b -> c -> d -> e -> f -> g -> h) -> a -> b -> c -> d -> e -> f -> g -> h
- killRange8 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h) => (a -> b -> c -> d -> e -> f -> g -> h -> i) -> a -> b -> c -> d -> e -> f -> g -> h -> i
- killRange9 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j
- killRange10 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k
- killRange11 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l
- killRange12 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m
- killRange13 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n
- killRange14 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o
- killRange15 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p
- killRange16 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q
- killRange17 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r
- killRange18 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q, KillRange r) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s
- killRange19 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q, KillRange r, KillRange s) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> t) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> 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 | |
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
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) | |
Show (Range' Integer) | |
Show a => Show (Range' (Maybe a)) | |
(Ord a, Arbitrary a) => Arbitrary (Range' a) | |
Null (Range' a) | |
Pretty a => Pretty (Range' (Maybe a)) | |
FreshName (Range, String) |
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.
newtype PrintRange a
Wrapper to indicate that range should be printed.
Constructors
PrintRange a |
Instances
Eq a => Eq (PrintRange a) | |
Ord a => Ord (PrintRange a) | |
(Pretty a, HasRange a) => Pretty (PrintRange a) | |
KillRange a => KillRange (PrintRange a) | |
SetRange a => SetRange (PrintRange a) | |
HasRange a => HasRange (PrintRange a) |
class HasRange t where
Things that have a range are instances of this class.
Instances
class HasRange t => SetRange t where
If it is also possible to set the range, this is the class.
Instances
SetRange Name | |
SetRange Range | |
SetRange QName | |
SetRange Name | |
SetRange ModuleName | |
SetRange QName | |
SetRange Literal | |
SetRange TypedBindings | |
SetRange Pattern | |
SetRange AbstractName | |
SetRange ConPatInfo | |
SetRange DeclInfo | |
SetRange DefInfo | |
SetRange ModuleInfo | |
SetRange ConHead | |
SetRange MetaInfo | |
SetRange MetaVariable | |
SetRange a => SetRange [a] | |
SetRange a => SetRange (PrintRange a) | |
SetRange a => SetRange (WithHiding a) | |
SetRange (Pattern' a) | |
SetRange a => SetRange (Named name a) | |
SetRange a => SetRange (Arg c a) |
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 -> b) -> a -> b
killRange2 :: (KillRange a, KillRange b) => (a -> b -> c) -> a -> b -> c
killRange3 :: (KillRange a, KillRange b, KillRange c) => (a -> b -> c -> d) -> a -> b -> c -> d
killRange4 :: (KillRange a, KillRange b, KillRange c, KillRange d) => (a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange5 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e) => (a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
killRange6 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f) => (a -> b -> c -> d -> e -> f -> g) -> a -> b -> c -> d -> e -> f -> g
killRange7 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g) => (a -> b -> c -> d -> e -> f -> g -> h) -> a -> b -> c -> d -> e -> f -> g -> h
killRange8 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h) => (a -> b -> c -> d -> e -> f -> g -> h -> i) -> a -> b -> c -> d -> e -> f -> g -> h -> i
killRange9 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j
killRange10 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k
killRange11 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l
killRange12 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m
killRange13 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n
killRange14 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o
killRange15 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p
killRange16 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q
killRange17 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r
killRange18 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q, KillRange r) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s
killRange19 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q, KillRange r, KillRange s) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> t) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> 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.