Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Syntax.Position

Contents

- Positions
- Intervals
- Ranges
- Tests

Description

Position information for syntax. Crucial for giving good error messages.

Synopsis

- type Position = Position' SrcFile
- data Position' a = Pn {
  - srcFile :: a
  - posPos :: !Int32
  - posLine :: !Int32
  - posCol :: !Int32
  }
- positionInvariant :: Position -> Bool
- startPos :: Maybe AbsolutePath -> Position
- movePos :: Position -> Char -> Position
- movePosByString :: Position -> String -> Position
- backupPos :: Position -> Position
- type Interval = Interval' SrcFile
- data Interval' a = Interval {
  - iStart :: !(Position' a)
  - iEnd :: !(Position' a)
  }
- intervalInvariant :: Interval -> Bool
- takeI :: String -> Interval -> Interval
- dropI :: String -> Interval -> Interval
- type Range = Range' SrcFile
- newtype Range' a = Range [Interval' a]
- rangeInvariant :: Range -> Bool
- noRange :: Range
- posToRange :: Position -> Position -> Range
- rStart :: Range -> Maybe Position
- rEnd :: Range -> Maybe Position
- rangeToInterval :: Range' a -> Maybe (Interval' a)
- 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 a1, KillRange a) => (a1 -> a -> t) -> a1 -> a -> t
- killRange3 :: (KillRange a2, KillRange a, KillRange a1) => (a2 -> a1 -> a -> t) -> a2 -> a1 -> a -> t
- killRange4 :: (KillRange a3, KillRange a1, KillRange a, KillRange a2) => (a3 -> a2 -> a1 -> a -> t) -> a3 -> a2 -> a1 -> a -> t
- killRange5 :: (KillRange a4, KillRange a2, KillRange a, KillRange a1, KillRange a3) => (a4 -> a3 -> a2 -> a1 -> a -> t) -> a4 -> a3 -> a2 -> a1 -> a -> t
- killRange6 :: (KillRange a5, KillRange a3, KillRange a1, KillRange a, KillRange a2, KillRange a4) => (a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t
- killRange7 :: (KillRange a6, KillRange a4, KillRange a2, KillRange a, KillRange a1, KillRange a3, KillRange a5) => (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

type Position = Position' SrcFile

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 |

Fields

srcFile :: a

  File.

posPos :: !Int32

  Position.

posLine :: !Int32

  Line number, counting from 1.

posCol :: !Int32

  Column number, counting from 1.

Instances

Functor Position' |
Read Position |
Typeable1 Position' |
EmbPrj Position |
Eq a => Eq (Position' a) |
Ord a => Ord (Position' a) |
Show a => Show (Position' (Maybe a)) |
Arbitrary a => Arbitrary (Position' a) |

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

type Interval = Interval' SrcFile

data Interval' a

An interval. The `iEnd` position is not included in the interval.

Note the invariant which intervals have to satisfy: `intervalInvariant`.

Constructors

Interval |

Fields

iStart :: !(Position' a)
iEnd :: !(Position' a)

Instances

Functor Interval' |
Read Interval |
Typeable1 Interval' |
HasRange Interval |
EmbPrj Interval |
Eq a => Eq (Interval' a) |
Ord a => Ord (Interval' a) |
Show a => Show (Interval' (Maybe a)) |
(Arbitrary a, Ord a) => Arbitrary (Interval' a) |

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

type Range = Range' SrcFile

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`.

Constructors

Range [Interval' a] |

Instances

Functor Range' |
Read Range |
Typeable1 Range' |
Arbitrary Range |
KillRange Range |
SetRange Range |
HasRange Range |
EmbPrj Range |
GenC Range |
Eq a => Eq (Range' a) |
Ord a => Ord (Range' a) |
Show a => Show (Range' (Maybe a)) |

rangeInvariant :: Range -> Bool

noRange :: Range

Ranges between two unknown positions

posToRange :: Position -> Position -> Range

Converts two positions to a range.

rStart :: Range -> Maybe Position

The initial position in the range, if any.

rEnd :: Range -> Maybe Position

The position after the final position in the range, if any.

rangeToInterval :: Range' a -> Maybe (Interval' a)

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.

Methods

getRange :: t -> Range

Instances

HasRange Range |
HasRange Interval |
HasRange Induction |
HasRange QName |
HasRange Name |
HasRange Fixity |
HasRange AmbiguousQName |
HasRange ModuleName |
HasRange QName |
HasRange Name |
HasRange Literal |
HasRange Pragma |
HasRange ModuleApplication |
HasRange Declaration |
HasRange AsName |
HasRange Renaming |
HasRange ImportedName |
HasRange UsingOrHiding |
HasRange ImportDirective |
HasRange WhereClause |
HasRange RHS |
HasRange LHSCore |
HasRange LHS |
HasRange TypedBinding |
HasRange BoundName |
HasRange TypedBindings |
HasRange LamBinding |
HasRange Pattern |
HasRange Expr |
HasRange Token |
HasRange AbstractName |
HasRange Clause |
HasRange PatInfo |
HasRange LHSInfo |
HasRange MutualInfo |
HasRange DeclInfo |
HasRange DefInfo |
HasRange LetInfo |
HasRange ModuleInfo |
HasRange ExprInfo |
HasRange MetaInfo |
HasRange LHS |
HasRange RHS |
HasRange Clause |
HasRange TypedBinding |
HasRange TypedBindings |
HasRange LamBinding |
HasRange LetBinding |
HasRange Declaration |
HasRange Expr |
HasRange DeclarationException |
HasRange NiceDeclaration |
HasRange ParseError |
HasRange TCErr |
HasRange Call |
HasRange MetaVariable |
HasRange ProjEntry |
HasRange a => HasRange [a] |
HasRange a => HasRange (Maybe a) |
HasRange a => HasRange (Arg a) |
HasRange a => HasRange (Dom a) |
HasRange e => HasRange (OpApp e) |
HasRange (Pattern' e) |
HasRange (LHSCore' e) |
HasRange a => HasRange (Closure a) |
(HasRange a, HasRange b) => HasRange (a, b) |
HasRange a => HasRange (Named name a) |
(HasRange a, HasRange b, HasRange c) => HasRange (a, b, c) |
(HasRange a, HasRange b, HasRange c, HasRange d) => HasRange (a, b, c, d) |
(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e) => HasRange (a, b, c, d, e) |
(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f) => HasRange (a, b, c, d, e, f) |
(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f, HasRange g) => HasRange (a, b, c, d, e, f, g) |

class HasRange t => SetRange t where

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

Instances

SetRange Range |
SetRange QName |
SetRange Name |
SetRange ModuleName |
SetRange QName |
SetRange Name |
SetRange Literal |
SetRange AbstractName |
SetRange DeclInfo |
SetRange DefInfo |
SetRange ModuleInfo |
SetRange MetaVariable |
SetRange (Pattern' a) |

class KillRange a where

Killing the range of an object sets all range information to `noRange`.

Methods

killRange :: a -> a

Instances

KillRange Range |
KillRange Relevance |
KillRange Hiding |
KillRange Induction |
KillRange Delayed |
KillRange QName |
KillRange Name |
KillRange Fixity |
KillRange Fixity' |
KillRange AmbiguousQName |
KillRange ModuleName |
KillRange QName |
KillRange Name |
KillRange Literal |
KillRange Pragma |
KillRange ModuleApplication |
KillRange Declaration |
KillRange AsName |
KillRange Renaming |
KillRange ImportedName |
KillRange UsingOrHiding |
KillRange ImportDirective |
KillRange WhereClause |
KillRange RHS |
KillRange LHS |
KillRange TypedBinding |
KillRange BoundName |
KillRange TypedBindings |
KillRange LamBinding |
KillRange Pattern |
KillRange Expr |
KillRange ScopeInfo |
KillRange LevelAtom |
KillRange PlusLevel |
KillRange Level |
KillRange Sort |
KillRange Type |
KillRange Term |
KillRange PatInfo |
KillRange LHSInfo |
KillRange MutualInfo |
KillRange DeclInfo |
KillRange DefInfo |
KillRange LetInfo |
KillRange ModuleInfo |
KillRange ExprInfo |
KillRange MetaInfo |
KillRange LHS |
KillRange RHS |
KillRange Clause |
KillRange TypedBinding |
KillRange TypedBindings |
KillRange LamBinding |
KillRange LetBinding |
KillRange ModuleApplication |
KillRange Declaration |
KillRange Expr |
KillRange Substitution |
KillRange a => KillRange [a] |
KillRange a => KillRange (Maybe a) |
KillRange a => KillRange (Arg a) |
KillRange a => KillRange (Dom a) |
KillRange x => KillRange (ThingWithFixity x) |
KillRange e => KillRange (OpApp e) |
KillRange a => KillRange (Blocked a) |
KillRange a => KillRange (Tele a) |
KillRange a => KillRange (Abs a) |
KillRange e => KillRange (Pattern' e) |
KillRange e => KillRange (LHSCore' e) |
(KillRange a, KillRange b) => KillRange (Either a b) |
(KillRange a, KillRange b) => KillRange (a, b) |
KillRange a => KillRange (Named name a) |
(KillRange a, KillRange b, KillRange c) => KillRange (a, b, c) |

killRange1 :: KillRange a => (a -> t) -> a -> t

killRange2 :: (KillRange a1, KillRange a) => (a1 -> a -> t) -> a1 -> a -> t

killRange3 :: (KillRange a2, KillRange a, KillRange a1) => (a2 -> a1 -> a -> t) -> a2 -> a1 -> a -> t

killRange4 :: (KillRange a3, KillRange a1, KillRange a, KillRange a2) => (a3 -> a2 -> a1 -> a -> t) -> a3 -> a2 -> a1 -> a -> t

killRange5 :: (KillRange a4, KillRange a2, KillRange a, KillRange a1, KillRange a3) => (a4 -> a3 -> a2 -> a1 -> a -> t) -> a4 -> a3 -> a2 -> a1 -> a -> t

killRange6 :: (KillRange a5, KillRange a3, KillRange a1, KillRange a, KillRange a2, KillRange a4) => (a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t

killRange7 :: (KillRange a6, KillRange a4, KillRange a2, KillRange a, KillRange a1, KillRange a3, KillRange a5) => (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 `withRangeOf` y` sets the range of `x` to the range of `y`.

fuseRange :: (HasRange u, HasRange t) => u -> t -> Range

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.

# Tests

tests :: IO Bool

Test suite.