Agda-2.4.0.2: 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 Source

data Position' a Source

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

startPos :: Maybe AbsolutePath -> Position Source

The first position in a file: position 1, line 1, column 1.

movePos :: Position' a -> Char -> Position' a Source

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 Source

Advance the position by a string.

movePosByString = foldl' movePos

backupPos :: Position' a -> Position' a Source

Backup the position by one character.

Precondition: The character must not be '\n'.

Intervals

type Interval = Interval' SrcFile Source

data Interval' a Source

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

takeI :: String -> Interval' a -> Interval' a Source

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 Source

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 Source

newtype Range' a Source

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

rightMargin :: Range -> Range Source

Conflate a range to its right margin.

noRange :: Range' a Source

Ranges between two unknown positions

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

Converts two positions to a range.

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

The initial position in the range, if any.

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

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

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

Converts a range to an interval, if possible.

continuous :: Range' a -> Range' a Source

Returns the shortest continuous range containing the given one.

continuousPerLine :: Ord a => Range' a -> Range' a Source

Removes gaps between intervals on the same line.

class HasRange t where Source

Things that have a range are instances of this class.

Methods

getRange :: t -> Range Source

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 Source

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 Source

Instances

class KillRange a where Source

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

Methods

killRange :: KillRangeT a Source

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 Source

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

killRange2 :: (KillRange s, KillRange a) => (s -> a -> t) -> s -> a -> t Source

killRange3 :: (KillRange s1, KillRange s, KillRange a) => (s1 -> s -> a -> t) -> s1 -> s -> a -> t Source

killRange4 :: (KillRange s2, KillRange s1, KillRange s, KillRange a) => (s2 -> s1 -> s -> a -> t) -> s2 -> s1 -> s -> a -> t Source

killRange5 :: (KillRange s3, KillRange s2, KillRange s1, KillRange s, KillRange a) => (s3 -> s2 -> s1 -> s -> a -> t) -> s3 -> s2 -> s1 -> s -> a -> t Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

withRangeOf :: (SetRange t, HasRange u) => t -> u -> t Source

x `withRangeOf` y sets the range of x to the range of y.

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

fuseRanges :: Ord a => Range' a -> Range' a -> Range' a Source

fuseRanges r r' unions the ranges r and r'.

Meaning it finds the least range r0 that covers r and r'.

beginningOf :: Range -> Range Source

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 Source

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 Source

Test suite.