Agda.Syntax.Position

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

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, counting from 1.

posLine :: !Int32

Line number, counting from 1.

posCol :: !Int32

Column number, counting from 1.

Instances

Functor Position'

Typeable1 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)

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

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'

Typeable1 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)

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

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'

Typeable1 Range'

Foldable Range'

Traversable Range'

KillRange Range

SetRange Range

HasRange 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)

rangeInvariant :: Range -> Bool

rightMargin :: Range -> Range

Conflate a range to its right margin.

noRange :: Range' a

Ranges between two unknown positions

posToRange :: Ord a => Position' a -> Position' a -> Range' a

Converts two positions to a range.

rStart :: Range' a -> Maybe (Position' a)

The initial position in the range, if any.

rEnd :: Range' a -> Maybe (Position' a)

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

Methods

getRange :: t -> Range

Instances

HasRange Range

HasRange Interval

HasRange Induction

HasRange ParseError

HasRange QName

HasRange Name

HasRange Fixity

HasRange AmbiguousQName

HasRange ModuleName

HasRange QName

HasRange Name

HasRange Literal

HasRange Token

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 AbstractName

HasRange ConPatInfo

HasRange PatInfo

HasRange LHSInfo

HasRange MutualInfo

HasRange DeclInfo

HasRange DefInfo

HasRange LetInfo

HasRange ModuleInfo

HasRange ExprInfo

HasRange MetaInfo

HasRange LHS

HasRange SpineLHS

HasRange RHS

HasRange TypedBinding

HasRange TypedBindings

HasRange LamBinding

HasRange LetBinding

HasRange Declaration

HasRange Expr

HasRange Clause

HasRange ConHead

HasRange DeclarationException

HasRange NiceDeclaration

HasRange TCErr

HasRange Call

HasRange MetaInfo

HasRange MetaVariable

HasRange Constraint

HasRange ProblemConstraint

HasRange a => HasRange [a]

HasRange a => HasRange (Maybe a)

HasRange (Ranged a)

HasRange e => HasRange (OpApp e)

HasRange (Pattern' e)

HasRange (LHSCore' e)

HasRange a => HasRange (Clause' a)

HasRange a => HasRange (Closure a)

IsExpr e => HasRange (ExprView e)

(HasRange a, HasRange b) => HasRange (a, b)

HasRange a => HasRange (Named name a)

HasRange a => HasRange (Dom c a)

HasRange a => HasRange (Arg c 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 ConPatInfo

SetRange DeclInfo

SetRange DefInfo

SetRange ModuleInfo

SetRange ConHead

SetRange MetaInfo

SetRange MetaVariable

SetRange (Pattern' a)

class KillRange a where

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

Methods

killRange :: KillRangeT a

Instances

KillRange Bool

KillRange Int

KillRange String

Overlaps with KillRange [a].

KillRange ()

KillRange Permutation

KillRange Range

KillRange InteractionId

KillRange IsAbstract

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 ConPatInfo

KillRange PatInfo

KillRange LHSInfo

KillRange MutualInfo

KillRange DeclInfo

KillRange DefInfo

KillRange LetInfo

KillRange ModuleInfo

KillRange ExprInfo

KillRange MetaInfo

KillRange LHS

KillRange SpineLHS

KillRange RHS

KillRange TypedBinding

KillRange TypedBindings

KillRange LamBinding

KillRange LetBinding

KillRange ModuleApplication

KillRange Declaration

KillRange Expr

KillRange Pattern

KillRange Clause

KillRange LevelAtom

KillRange PlusLevel

KillRange Level

KillRange Sort

KillRange Type

KillRange Term

KillRange ConHead

KillRange CompiledClauses

KillRange MutualId

KillRange TermHead

KillRange Defn

KillRange Projection

KillRange Occurrence

KillRange CompiledRepresentation

KillRange Polarity

KillRange Definition

KillRange DisplayTerm

KillRange DisplayForm

KillRange Section

KillRange Definitions

KillRange Sections

KillRange Signature

KillRange Substitution

KillRange a => KillRange [a]

KillRange a => KillRange (Maybe a)

KillRange a => KillRange (Drop a)

KillRange (Ranged a)

KillRange c => KillRange (ArgInfo c)

KillRange x => KillRange (ThingWithFixity x)

KillRange e => KillRange (OpApp e)

KillRange e => KillRange (Pattern' e)

KillRange e => KillRange (LHSCore' e)

KillRange a => KillRange (Clause' a)

KillRange a => KillRange (ClauseBodyF a)

KillRange a => KillRange (Blocked a)

KillRange a => KillRange (Tele a)

KillRange a => KillRange (Abs a)

KillRange a => KillRange (Elim' a)

KillRange c => KillRange (Case c)

KillRange c => KillRange (WithArity c)

KillRange c => KillRange (FunctionInverse' c)

KillRange a => KillRange (Open a)

(KillRange a, KillRange b) => KillRange (Either a b)

(KillRange a, KillRange b) => KillRange (a, b)

(KillRange name, KillRange a) => KillRange (Named name a)

(KillRange c, KillRange a) => KillRange (Dom c a)

(KillRange c, KillRange a) => KillRange (Arg c a)

(KillRange a, KillRange b, KillRange c) => KillRange (a, b, c)

type KillRangeT a = a -> a

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

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

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

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

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

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

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

killRange8 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5, KillRange a6, KillRange a7) => (a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t

killRange9 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5, KillRange a6, KillRange a7, KillRange a8) => (a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t

killRange10 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5, KillRange a6, KillRange a7, KillRange a8, KillRange a9) => (a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t

killRange11 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5, KillRange a6, KillRange a7, KillRange a8, KillRange a9, KillRange a10) => (a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t

killRange12 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5, KillRange a6, KillRange a7, KillRange a8, KillRange a9, KillRange a10, KillRange a11) => (a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t

killRange13 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5, KillRange a6, KillRange a7, KillRange a8, KillRange a9, KillRange a10, KillRange a11, KillRange a12) => (a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t

killRange14 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5, KillRange a6, KillRange a7, KillRange a8, KillRange a9, KillRange a10, KillRange a11, KillRange a12, KillRange a13) => (a13 -> a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a13 -> a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t

killRange15 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5, KillRange a6, KillRange a7, KillRange a8, KillRange a9, KillRange a10, KillRange a11, KillRange a12, KillRange a13, KillRange a14) => (a14 -> a13 -> a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a14 -> a13 -> a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t

killRange16 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5, KillRange a6, KillRange a7, KillRange a8, KillRange a9, KillRange a10, KillRange a11, KillRange a12, KillRange a13, KillRange a14, KillRange a15) => (a15 -> a14 -> a13 -> a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a15 -> a14 -> a13 -> a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t

killRange17 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5, KillRange a6, KillRange a7, KillRange a8, KillRange a9, KillRange a10, KillRange a11, KillRange a12, KillRange a13, KillRange a14, KillRange a15, KillRange a16) => (a16 -> a15 -> a14 -> a13 -> a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a16 -> a15 -> a14 -> a13 -> a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t

killRange18 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5, KillRange a6, KillRange a7, KillRange a8, KillRange a9, KillRange a10, KillRange a11, KillRange a12, KillRange a13, KillRange a14, KillRange a15, KillRange a16, KillRange a17) => (a17 -> a16 -> a15 -> a14 -> a13 -> a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a17 -> a16 -> a15 -> a14 -> a13 -> a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t

killRange19 :: (KillRange a, KillRange a1, KillRange a2, KillRange a3, KillRange a4, KillRange a5, KillRange a6, KillRange a7, KillRange a8, KillRange a9, KillRange a10, KillRange a11, KillRange a12, KillRange a13, KillRange a14, KillRange a15, KillRange a16, KillRange a17, KillRange a18) => (a18 -> a17 -> a16 -> a15 -> a14 -> a13 -> a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> a6 -> a5 -> a4 -> a3 -> a2 -> a1 -> a -> t) -> a18 -> a17 -> a16 -> a15 -> a14 -> a13 -> a12 -> a11 -> a10 -> a9 -> a8 -> a7 -> 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 :: 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.

Tests

tests :: IO Bool

Test suite.