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

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Position

Contents

Description

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

Synopsis

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.

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, iEnd :: !(Position' a)
 

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] 

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.

newtype PrintRange a

Wrapper to indicate that range should be printed.

Constructors

PrintRange a 

class HasRange t where

Things that have a range are instances of this class.

Methods

getRange :: t -> Range

Instances

HasRange Name 
HasRange Range 
HasRange Interval 
HasRange Induction 
HasRange QName 
HasRange Name 
HasRange Fixity 
HasRange AmbiguousQName

The range of an AmbiguousQName is the range of any of its disambiguations (they are the same concrete name).

HasRange ModuleName 
HasRange QName 
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 DeclarationException 
HasRange NiceDeclaration 
HasRange ParseError 
HasRange LHS 
HasRange SpineLHS 
HasRange RHS 
HasRange TypedBinding 
HasRange TypedBindings 
HasRange LamBinding 
HasRange LetBinding 
HasRange Declaration 
HasRange Expr 
HasRange Clause 
HasRange ConHead 
HasRange TCErr 
HasRange Call 
HasRange MetaInfo 
HasRange MetaVariable 
HasRange Constraint 
HasRange ProblemConstraint 
HasRange a => HasRange [a] 
HasRange a => HasRange (Maybe a) 
HasRange a => HasRange (PrintRange a) 
HasRange (Ranged a) 
HasRange a => HasRange (WithHiding 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 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 Integer 
KillRange () 
KillRange Fixity' 
KillRange Name 
KillRange Range 
KillRange InteractionId 
KillRange NameId 
KillRange IsAbstract 
KillRange Relevance 
KillRange Hiding 
KillRange Induction 
KillRange Delayed 
KillRange QName 
KillRange Name 
KillRange GenPart 
KillRange Fixity 
KillRange AmbiguousQName 
KillRange ModuleName 
KillRange QName 
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 Substitution 
KillRange ConPatternInfo 
KillRange Pattern 
KillRange Clause 
KillRange LevelAtom 
KillRange PlusLevel 
KillRange Level 
KillRange Sort 
KillRange Type 
KillRange Term 
KillRange ConHead 
KillRange a => KillRange [a] 
KillRange a => KillRange (Maybe a) 
(Ord a, KillRange a) => KillRange (Set a) 
KillRange a => KillRange (PrintRange a) 
KillRange m => KillRange (TerminationCheck m) 
KillRange (Ranged a) 
KillRange c => KillRange (ArgInfo c) 
KillRange a => KillRange (WithHiding a) 
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 a, KillRange b) => KillRange (Either a b) 
(KillRange a, KillRange b) => KillRange (a, b) 
KillRange a => KillRange (Map k a) 
(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) 
(KillRange a, KillRange b, KillRange c, KillRange d) => KillRange (a, b, c, d) 

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.

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.