Agda-2.4.2.5: 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' Source 
Foldable Position' Source 
Traversable Position' Source 
Eq a => Eq (Position' a) Source 
Ord a => Ord (Position' a) Source 
Show (Position' Integer) Source 
Show a => Show (Position' (Maybe a)) Source 
Arbitrary a => Arbitrary (Position' a) Source 
Pretty a => Pretty (Position' (Maybe a)) Source 

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

Instances

Functor Interval' Source 
Foldable Interval' Source 
Traversable Interval' Source 
HasRange Interval Source 
Eq a => Eq (Interval' a) Source 
Ord a => Ord (Interval' a) Source 
Show (Interval' Integer) Source 
Show a => Show (Interval' (Maybe a)) Source 
(Arbitrary a, Ord a) => Arbitrary (Interval' a) Source 
Pretty a => Pretty (Interval' (Maybe a)) Source 

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' Source 
Foldable Range' Source 
Traversable Range' Source 
KillRange Range Source 
SetRange Range Source 
HasRange Range Source 
FreshName Range Source 
GenC Range Source 
PrettyTCM Range Source 
Eq a => Eq (Range' a) Source 
Ord a => Ord (Range' a) Source 
Show (Range' Integer) Source 
Show a => Show (Range' (Maybe a)) Source 
(Ord a, Arbitrary a) => Arbitrary (Range' a) Source 
Null (Range' a) Source 
Pretty a => Pretty (Range' (Maybe a)) Source 
FreshName (Range, String) Source 

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.

newtype PrintRange a Source

Wrapper to indicate that range should be printed.

Constructors

PrintRange a 

Instances

class HasRange t where Source

Things that have a range are instances of this class.

Methods

getRange :: t -> Range Source

Instances

HasRange Range Source 
HasRange Interval Source 
HasRange Induction Source 
HasRange QName Source 
HasRange Name Source 
HasRange AmbiguousQName Source

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

HasRange ModuleName Source 
HasRange QName Source 
HasRange Name Source 
HasRange Literal Source 
HasRange Token Source 
HasRange Fixity Source 
HasRange Pragma Source 
HasRange ModuleApplication Source 
HasRange Declaration Source 
HasRange AsName Source 
HasRange Renaming Source 
HasRange ImportedName Source 
HasRange UsingOrHiding Source 
HasRange ImportDirective Source 
HasRange WhereClause Source 
HasRange RHS Source 
HasRange LHSCore Source 
HasRange LHS Source 
HasRange TypedBinding Source 
HasRange BoundName Source 
HasRange TypedBindings Source 
HasRange LamBinding Source 
HasRange Pattern Source 
HasRange Expr Source 
HasRange AbstractName Source 
HasRange ConPatInfo Source 
HasRange PatInfo Source 
HasRange LHSInfo Source 
HasRange MutualInfo Source 
HasRange DeclInfo Source 
HasRange DefInfo Source 
HasRange LetInfo Source 
HasRange ModuleInfo Source 
HasRange ExprInfo Source 
HasRange MetaInfo Source 
HasRange DeclarationException Source 
HasRange NiceDeclaration Source 
HasRange ParseError Source 
HasRange LHS Source 
HasRange SpineLHS Source 
HasRange RHS Source 
HasRange TypedBinding Source 
HasRange TypedBindings Source 
HasRange LamBinding Source 
HasRange LetBinding Source 
HasRange Declaration Source 
HasRange Expr Source 
HasRange Clause Source 
HasRange ConHead Source 
HasRange TCErr Source 
HasRange Call Source 
HasRange MetaInfo Source 
HasRange MetaVariable Source 
HasRange Constraint Source 
HasRange ProblemConstraint Source 
HasRange a => HasRange [a] Source 
HasRange a => HasRange (Maybe a) Source 
HasRange a => HasRange (PrintRange a) Source 
HasRange (Ranged a) Source 
HasRange a => HasRange (WithHiding a) Source 
HasRange e => HasRange (OpApp e) Source 
HasRange (Pattern' e) Source 
HasRange (LHSCore' e) Source 
HasRange a => HasRange (Clause' a) Source 
HasRange a => HasRange (Closure a) Source 
IsExpr e => HasRange (ExprView e) Source 
(HasRange a, HasRange b) => HasRange (a, b) Source 
HasRange a => HasRange (Named name a) Source 
HasRange a => HasRange (Dom c a) Source 
HasRange a => HasRange (Arg c a) Source 
(HasRange a, HasRange b, HasRange c) => HasRange (a, b, c) Source 
(HasRange a, HasRange b, HasRange c, HasRange d) => HasRange (a, b, c, d) Source 
(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e) => HasRange (a, b, c, d, e) Source 
(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f) => HasRange (a, b, c, d, e, f) Source 
(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f, HasRange g) => HasRange (a, b, c, d, e, f, g) Source 

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 Source 
KillRange Int Source 
KillRange Integer Source 
KillRange String Source

Overlaps with KillRange [a].

KillRange () Source 
KillRange Range Source 
KillRange InteractionId Source 
KillRange NameId Source 
KillRange IsAbstract Source 
KillRange Relevance Source 
KillRange Hiding Source 
KillRange Induction Source 
KillRange Delayed Source 
KillRange QName Source 
KillRange Name Source 
KillRange Fixity' Source 
KillRange AmbiguousQName Source 
KillRange ModuleName Source 
KillRange QName Source 
KillRange Name Source 
KillRange Literal Source 
KillRange GenPart Source 
KillRange Fixity Source 
KillRange Pragma Source 
KillRange ModuleApplication Source 
KillRange Declaration Source 
KillRange AsName Source 
KillRange Renaming Source 
KillRange ImportedName Source 
KillRange UsingOrHiding Source 
KillRange ImportDirective Source 
KillRange WhereClause Source 
KillRange RHS Source 
KillRange LHS Source 
KillRange TypedBinding Source 
KillRange BoundName Source 
KillRange TypedBindings Source 
KillRange LamBinding Source 
KillRange Pattern Source 
KillRange Expr Source 
KillRange ScopeInfo Source 
KillRange ConPatInfo Source 
KillRange PatInfo Source 
KillRange LHSInfo Source 
KillRange MutualInfo Source 
KillRange DeclInfo Source 
KillRange DefInfo Source 
KillRange LetInfo Source 
KillRange ModuleInfo Source 
KillRange ExprInfo Source 
KillRange MetaInfo Source 
KillRange Occurrence Source 
KillRange LHS Source 
KillRange SpineLHS Source 
KillRange RHS Source 
KillRange TypedBinding Source 
KillRange TypedBindings Source 
KillRange LamBinding Source 
KillRange LetBinding Source 
KillRange ModuleApplication Source 
KillRange Declaration Source 
KillRange Expr Source 
KillRange Permutation Source 
KillRange Substitution Source 
KillRange ConPatternInfo Source 
KillRange Pattern Source 
KillRange Clause Source 
KillRange LevelAtom Source 
KillRange PlusLevel Source 
KillRange Level Source 
KillRange Sort Source 
KillRange Term Source 
KillRange ConHead Source 
KillRange CompiledClauses Source 
KillRange MutualId Source 
KillRange TermHead Source 
KillRange Defn Source 
KillRange Projection Source 
KillRange ExtLamInfo Source 
KillRange CompiledRepresentation Source 
KillRange Polarity Source 
KillRange Definition Source 
KillRange RewriteRule Source 
KillRange NLPat Source 
KillRange DisplayTerm Source 
KillRange DisplayForm Source 
KillRange Section Source 
KillRange RewriteRuleMap Source 
KillRange Definitions Source 
KillRange Sections Source 
KillRange Signature Source 
KillRange a => KillRange [a] Source 
KillRange a => KillRange (Maybe a) Source 
(Ord a, KillRange a) => KillRange (Set a) Source 
KillRange a => KillRange (PrintRange a) Source 
KillRange m => KillRange (TerminationCheck m) Source 
KillRange (Ranged a) Source 
KillRange c => KillRange (ArgInfo c) Source 
KillRange a => KillRange (WithHiding a) Source 
KillRange x => KillRange (ThingWithFixity x) Source 
KillRange e => KillRange (OpApp e) Source 
KillRange e => KillRange (Pattern' e) Source 
KillRange e => KillRange (LHSCore' e) Source 
KillRange a => KillRange (Clause' a) Source 
KillRange a => KillRange (Drop a) Source 
KillRange a => KillRange (ClauseBodyF a) Source 
KillRange a => KillRange (Blocked a) Source 
KillRange a => KillRange (Tele a) Source 
KillRange a => KillRange (Type' a) Source 
KillRange a => KillRange (Abs a) Source 
KillRange a => KillRange (Elim' a) Source 
KillRange c => KillRange (Case c) Source 
KillRange c => KillRange (WithArity c) Source 
KillRange c => KillRange (FunctionInverse' c) Source 
KillRange a => KillRange (Open a) Source 
(KillRange a, KillRange b) => KillRange (Either a b) Source 
(KillRange a, KillRange b) => KillRange (a, b) Source 
KillRange a => KillRange (Map k a) Source 
(KillRange name, KillRange a) => KillRange (Named name a) Source 
(KillRange c, KillRange a) => KillRange (Dom c a) Source 
(KillRange c, KillRange a) => KillRange (Arg c a) Source 
(KillRange a, KillRange b, KillRange c) => KillRange (a, b, c) Source 
(KillRange a, KillRange b, KillRange c, KillRange d) => KillRange (a, b, c, d) Source 

type KillRangeT a = a -> a Source

killRangeMap :: (KillRange k, KillRange v) => KillRangeT (Map k v) Source

Remove ranges in keys and values of a map.

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

killRange2 :: (KillRange a, KillRange b) => (a -> b -> c) -> a -> b -> c Source

killRange3 :: (KillRange a, KillRange b, KillRange c) => (a -> b -> c -> d) -> a -> b -> c -> d Source

killRange4 :: (KillRange a, KillRange b, KillRange c, KillRange d) => (a -> b -> c -> d -> e) -> a -> b -> c -> d -> e Source

killRange5 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e) => (a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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