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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Position

Contents

Description

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

Synopsis

Positions

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

Instances

Functor Position' # 

Methods

fmap :: (a -> b) -> Position' a -> Position' b #

(<$) :: a -> Position' b -> Position' a #

Show PositionWithoutFile # 
Foldable Position' # 

Methods

fold :: Monoid m => Position' m -> m #

foldMap :: Monoid m => (a -> m) -> Position' a -> m #

foldr :: (a -> b -> b) -> b -> Position' a -> b #

foldr' :: (a -> b -> b) -> b -> Position' a -> b #

foldl :: (b -> a -> b) -> b -> Position' a -> b #

foldl' :: (b -> a -> b) -> b -> Position' a -> b #

foldr1 :: (a -> a -> a) -> Position' a -> a #

foldl1 :: (a -> a -> a) -> Position' a -> a #

toList :: Position' a -> [a] #

null :: Position' a -> Bool #

length :: Position' a -> Int #

elem :: Eq a => a -> Position' a -> Bool #

maximum :: Ord a => Position' a -> a #

minimum :: Ord a => Position' a -> a #

sum :: Num a => Position' a -> a #

product :: Num a => Position' a -> a #

Traversable Position' # 

Methods

traverse :: Applicative f => (a -> f b) -> Position' a -> f (Position' b) #

sequenceA :: Applicative f => Position' (f a) -> f (Position' a) #

mapM :: Monad m => (a -> m b) -> Position' a -> m (Position' b) #

sequence :: Monad m => Position' (m a) -> m (Position' a) #

Pretty PositionWithoutFile # 
Eq a => Eq (Position' a) # 

Methods

(==) :: Position' a -> Position' a -> Bool #

(/=) :: Position' a -> Position' a -> Bool #

Ord a => Ord (Position' a) # 
Show a => Show (Position' (Maybe a)) # 
Generic (Position' a) # 

Associated Types

type Rep (Position' a) :: * -> * #

Methods

from :: Position' a -> Rep (Position' a) x #

to :: Rep (Position' a) x -> Position' a #

Pretty a => Pretty (Position' (Maybe a)) # 

Methods

pretty :: Position' (Maybe a) -> Doc #

prettyPrec :: Int -> Position' (Maybe a) -> Doc #

type Rep (Position' a) # 

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

startPos' :: a -> Position' a #

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

Intervals

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

Instances

Functor Interval' # 

Methods

fmap :: (a -> b) -> Interval' a -> Interval' b #

(<$) :: a -> Interval' b -> Interval' a #

Show IntervalWithoutFile # 
Foldable Interval' # 

Methods

fold :: Monoid m => Interval' m -> m #

foldMap :: Monoid m => (a -> m) -> Interval' a -> m #

foldr :: (a -> b -> b) -> b -> Interval' a -> b #

foldr' :: (a -> b -> b) -> b -> Interval' a -> b #

foldl :: (b -> a -> b) -> b -> Interval' a -> b #

foldl' :: (b -> a -> b) -> b -> Interval' a -> b #

foldr1 :: (a -> a -> a) -> Interval' a -> a #

foldl1 :: (a -> a -> a) -> Interval' a -> a #

toList :: Interval' a -> [a] #

null :: Interval' a -> Bool #

length :: Interval' a -> Int #

elem :: Eq a => a -> Interval' a -> Bool #

maximum :: Ord a => Interval' a -> a #

minimum :: Ord a => Interval' a -> a #

sum :: Num a => Interval' a -> a #

product :: Num a => Interval' a -> a #

Traversable Interval' # 

Methods

traverse :: Applicative f => (a -> f b) -> Interval' a -> f (Interval' b) #

sequenceA :: Applicative f => Interval' (f a) -> f (Interval' a) #

mapM :: Monad m => (a -> m b) -> Interval' a -> m (Interval' b) #

sequence :: Monad m => Interval' (m a) -> m (Interval' a) #

Pretty IntervalWithoutFile # 
HasRange Interval # 

Methods

getRange :: Interval -> Range #

Eq a => Eq (Interval' a) # 

Methods

(==) :: Interval' a -> Interval' a -> Bool #

(/=) :: Interval' a -> Interval' a -> Bool #

Ord a => Ord (Interval' a) # 
Show a => Show (Interval' (Maybe a)) # 
Generic (Interval' a) # 

Associated Types

type Rep (Interval' a) :: * -> * #

Methods

from :: Interval' a -> Rep (Interval' a) x #

to :: Rep (Interval' a) x -> Interval' a #

Pretty a => Pretty (Interval' (Maybe a)) # 

Methods

pretty :: Interval' (Maybe a) -> Doc #

prettyPrec :: Int -> Interval' (Maybe a) -> Doc #

type Rep (Interval' a) # 
type Rep (Interval' a) = D1 (MetaData "Interval'" "Agda.Syntax.Position" "Agda-2.5.2-75ei4uCcbjhBaJJCNAC8Q3" False) (C1 (MetaCons "Interval" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "iStart") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (Position' a))) (S1 (MetaSel (Just Symbol "iEnd") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (Position' a)))))

posToInterval :: a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a #

Converts a file name and two positions to an interval.

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.

getIntervalFile :: Interval' a -> a #

Gets the srcFile component of the interval. Because of the invariant, they are both the same.

iLength :: Interval' a -> Int32 #

The length of an interval.

fuseIntervals :: Ord a => Interval' a -> Interval' a -> Interval' a #

Finds the least interval which covers the arguments.

Precondition: The intervals must point to the same file.

setIntervalFile :: a -> Interval' b -> Interval' a #

Sets the srcFile components of the interval.

Ranges

data Range' a #

A range is a file name, plus a sequence of intervals, assumed to point to the given file. The intervals should be consecutive and separated.

Note the invariant which ranges have to satisfy: rangeInvariant.

Constructors

NoRange 
Range !a (Seq IntervalWithoutFile) 

Instances

Functor Range' # 

Methods

fmap :: (a -> b) -> Range' a -> Range' b #

(<$) :: a -> Range' b -> Range' a #

Foldable Range' # 

Methods

fold :: Monoid m => Range' m -> m #

foldMap :: Monoid m => (a -> m) -> Range' a -> m #

foldr :: (a -> b -> b) -> b -> Range' a -> b #

foldr' :: (a -> b -> b) -> b -> Range' a -> b #

foldl :: (b -> a -> b) -> b -> Range' a -> b #

foldl' :: (b -> a -> b) -> b -> Range' a -> b #

foldr1 :: (a -> a -> a) -> Range' a -> a #

foldl1 :: (a -> a -> a) -> Range' a -> a #

toList :: Range' a -> [a] #

null :: Range' a -> Bool #

length :: Range' a -> Int #

elem :: Eq a => a -> Range' a -> Bool #

maximum :: Ord a => Range' a -> a #

minimum :: Ord a => Range' a -> a #

sum :: Num a => Range' a -> a #

product :: Num a => Range' a -> a #

Traversable Range' # 

Methods

traverse :: Applicative f => (a -> f b) -> Range' a -> f (Range' b) #

sequenceA :: Applicative f => Range' (f a) -> f (Range' a) #

mapM :: Monad m => (a -> m b) -> Range' a -> m (Range' b) #

sequence :: Monad m => Range' (m a) -> m (Range' a) #

KillRange Range # 
SetRange Range # 

Methods

setRange :: Range -> Range -> Range #

HasRange Range # 

Methods

getRange :: Range -> Range #

FreshName Range # 
PrettyTCM Range # 

Methods

prettyTCM :: Range -> TCM Doc #

Eq a => Eq (Range' a) # 

Methods

(==) :: Range' a -> Range' a -> Bool #

(/=) :: Range' a -> Range' a -> Bool #

Ord a => Ord (Range' a) # 

Methods

compare :: Range' a -> Range' a -> Ordering #

(<) :: Range' a -> Range' a -> Bool #

(<=) :: Range' a -> Range' a -> Bool #

(>) :: Range' a -> Range' a -> Bool #

(>=) :: Range' a -> Range' a -> Bool #

max :: Range' a -> Range' a -> Range' a #

min :: Range' a -> Range' a -> Range' a #

Show a => Show (Range' (Maybe a)) # 

Methods

showsPrec :: Int -> Range' (Maybe a) -> ShowS #

show :: Range' (Maybe a) -> String #

showList :: [Range' (Maybe a)] -> ShowS #

Show a => Show (Range' (Maybe a)) # 

Methods

showsPrec :: Int -> Range' (Maybe a) -> ShowS #

show :: Range' (Maybe a) -> String #

showList :: [Range' (Maybe a)] -> ShowS #

Generic (Range' a) # 

Associated Types

type Rep (Range' a) :: * -> * #

Methods

from :: Range' a -> Rep (Range' a) x #

to :: Rep (Range' a) x -> Range' a #

Pretty a => Pretty (Range' (Maybe a)) # 

Methods

pretty :: Range' (Maybe a) -> Doc #

prettyPrec :: Int -> Range' (Maybe a) -> Doc #

Null (Range' a) # 

Methods

empty :: Range' a #

null :: Range' a -> Bool #

FreshName (Range, String) # 
type Rep (Range' a) # 

rangeInvariant :: Ord a => Range' a -> Bool #

Range invariant.

consecutiveAndSeparated :: Ord a => [Interval' a] -> Bool #

Are the intervals consecutive and separated, do they all point to the same file, and do they satisfy the interval invariant?

intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a #

Turns a file name plus a list of intervals into a range.

Precondition: consecutiveAndSeparated.

intervalToRange :: a -> IntervalWithoutFile -> Range' a #

Converts a file name and an interval to a range.

rangeIntervals :: Range' a -> [IntervalWithoutFile] #

The intervals that make up the range. The intervals are consecutive and separated (consecutiveAndSeparated).

rangeFile :: Range -> SrcFile #

The file the range is pointing to.

rightMargin :: Range -> Range #

Conflate a range to its right margin.

noRange :: Range' a #

Ranges between two unknown positions

posToRange :: Position' a -> Position' a -> Range' a #

Converts two positions to a range.

Precondition: The positions have to point to the same file.

posToRange' :: a -> PositionWithoutFile -> PositionWithoutFile -> Range' a #

Converts a file name and two positions to a range.

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

The initial position in the range, if any.

rStart' :: Range' a -> Maybe PositionWithoutFile #

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.

rEnd' :: Range' a -> Maybe PositionWithoutFile #

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

rangeToInterval :: Range' a -> Maybe IntervalWithoutFile #

Converts a range to an interval, if possible. Note that the information about the source file is lost.

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

Minimal complete definition

getRange

Methods

getRange :: t -> Range #

Instances

HasRange Bool # 

Methods

getRange :: Bool -> Range #

HasRange Range # 

Methods

getRange :: Range -> Range #

HasRange Interval # 

Methods

getRange :: Interval -> Range #

HasRange ParseWarning # 
HasRange ParseError # 

Methods

getRange :: ParseError -> Range #

HasRange Layer # 

Methods

getRange :: Layer -> Range #

HasRange IsMacro # 

Methods

getRange :: IsMacro -> Range #

HasRange IsInstance # 

Methods

getRange :: IsInstance -> Range #

HasRange Access # 

Methods

getRange :: Access -> Range #

HasRange Induction # 

Methods

getRange :: Induction -> Range #

HasRange QName # 

Methods

getRange :: QName -> Range #

HasRange Name # 

Methods

getRange :: Name -> Range #

HasRange AmbiguousQName #

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

HasRange ModuleName # 

Methods

getRange :: ModuleName -> Range #

HasRange QName # 

Methods

getRange :: QName -> Range #

HasRange Name # 

Methods

getRange :: Name -> Range #

HasRange Fixity # 

Methods

getRange :: Fixity -> Range #

HasRange Literal # 

Methods

getRange :: Literal -> Range #

HasRange Token # 

Methods

getRange :: Token -> Range #

HasRange Pragma # 

Methods

getRange :: Pragma -> Range #

HasRange ModuleApplication # 
HasRange Declaration # 
HasRange AsName # 

Methods

getRange :: AsName -> Range #

HasRange WhereClause # 
HasRange RHS # 

Methods

getRange :: RHS -> Range #

HasRange LHSCore # 

Methods

getRange :: LHSCore -> Range #

HasRange LHS # 

Methods

getRange :: LHS -> Range #

HasRange TypedBinding # 
HasRange BoundName # 

Methods

getRange :: BoundName -> Range #

HasRange TypedBindings # 
HasRange LamBinding # 

Methods

getRange :: LamBinding -> Range #

HasRange Pattern # 

Methods

getRange :: Pattern -> Range #

HasRange Expr # 

Methods

getRange :: Expr -> Range #

HasRange ModuleAssignment # 
HasRange DeclarationException # 
HasRange NiceDeclaration # 
HasRange AbstractName # 
HasRange ConPatInfo # 

Methods

getRange :: ConPatInfo -> Range #

HasRange PatInfo # 

Methods

getRange :: PatInfo -> Range #

HasRange LHSInfo # 

Methods

getRange :: LHSInfo -> Range #

HasRange MutualInfo # 

Methods

getRange :: MutualInfo -> Range #

HasRange DeclInfo # 

Methods

getRange :: DeclInfo -> Range #

HasRange DefInfo # 

Methods

getRange :: DefInfo -> Range #

HasRange LetInfo # 

Methods

getRange :: LetInfo -> Range #

HasRange ModuleInfo # 

Methods

getRange :: ModuleInfo -> Range #

HasRange ExprInfo # 

Methods

getRange :: ExprInfo -> Range #

HasRange MetaInfo # 

Methods

getRange :: MetaInfo -> Range #

HasRange Clause # 

Methods

getRange :: Clause -> Range #

HasRange ConHead # 

Methods

getRange :: ConHead -> Range #

HasRange LHS # 

Methods

getRange :: LHS -> Range #

HasRange SpineLHS # 

Methods

getRange :: SpineLHS -> Range #

HasRange RHS # 

Methods

getRange :: RHS -> Range #

HasRange TypedBinding # 
HasRange TypedBindings # 
HasRange LamBinding # 

Methods

getRange :: LamBinding -> Range #

HasRange LetBinding # 

Methods

getRange :: LetBinding -> Range #

HasRange Declaration # 
HasRange Expr # 

Methods

getRange :: Expr -> Range #

HasRange TCErr # 

Methods

getRange :: TCErr -> Range #

HasRange Call # 

Methods

getRange :: Call -> Range #

HasRange MetaInfo # 

Methods

getRange :: MetaInfo -> Range #

HasRange MetaVariable # 
HasRange Constraint # 

Methods

getRange :: Constraint -> Range #

HasRange ProblemConstraint # 
HasRange Item # 

Methods

getRange :: Item -> Range #

HasRange a => HasRange [a] #

Precondition: The ranges of the list elements must point to the same file (or be empty).

Methods

getRange :: [a] -> Range #

HasRange a => HasRange (Maybe a) # 

Methods

getRange :: Maybe a -> Range #

HasRange a => HasRange (PrintRange a) # 

Methods

getRange :: PrintRange a -> Range #

HasRange a => HasRange (MaybePlaceholder a) # 
HasRange (Ranged a) # 

Methods

getRange :: Ranged a -> Range #

HasRange a => HasRange (Dom a) # 

Methods

getRange :: Dom a -> Range #

HasRange a => HasRange (Arg a) # 

Methods

getRange :: Arg a -> Range #

HasRange a => HasRange (WithHiding a) # 

Methods

getRange :: WithHiding a -> Range #

HasRange a => HasRange (FieldAssignment' a) # 
HasRange e => HasRange (OpApp e) # 

Methods

getRange :: OpApp e -> Range #

IsExpr e => HasRange (ExprView e) # 

Methods

getRange :: ExprView e -> Range #

HasRange (Pattern' e) # 

Methods

getRange :: Pattern' e -> Range #

HasRange (LHSCore' e) # 

Methods

getRange :: LHSCore' e -> Range #

HasRange a => HasRange (Clause' a) # 

Methods

getRange :: Clause' a -> Range #

HasRange a => HasRange (Closure a) # 

Methods

getRange :: Closure a -> Range #

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

Methods

getRange :: Either a b -> Range #

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

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Methods

getRange :: (a, b) -> Range #

(HasRange a, HasRange b) => HasRange (Renaming' a b) # 

Methods

getRange :: Renaming' a b -> Range #

(HasRange a, HasRange b) => HasRange (ImportedName' a b) # 

Methods

getRange :: ImportedName' a b -> Range #

(HasRange a, HasRange b) => HasRange (Using' a b) # 

Methods

getRange :: Using' a b -> Range #

(HasRange a, HasRange b) => HasRange (ImportDirective' a b) # 

Methods

getRange :: ImportDirective' a b -> Range #

HasRange a => HasRange (Named name a) # 

Methods

getRange :: Named name a -> Range #

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

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Methods

getRange :: (a, b, c) -> Range #

(HasRange a, HasRange b, HasRange c, HasRange d) => HasRange (a, b, c, d) #

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Methods

getRange :: (a, b, c, d) -> Range #

(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e) => HasRange (a, b, c, d, e) #

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Methods

getRange :: (a, b, c, d, e) -> Range #

(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f) => HasRange (a, b, c, d, e, f) #

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Methods

getRange :: (a, b, c, d, e, f) -> Range #

(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f, HasRange g) => HasRange (a, b, c, d, e, f, g) #

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Methods

getRange :: (a, b, c, d, e, f, g) -> Range #

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.

Minimal complete definition

setRange

Methods

setRange :: Range -> t -> t #

Instances

SetRange Range # 

Methods

setRange :: Range -> Range -> Range #

SetRange QName # 

Methods

setRange :: Range -> QName -> QName #

SetRange Name # 

Methods

setRange :: Range -> Name -> Name #

SetRange ModuleName # 
SetRange QName # 

Methods

setRange :: Range -> QName -> QName #

SetRange Name # 

Methods

setRange :: Range -> Name -> Name #

SetRange Literal # 

Methods

setRange :: Range -> Literal -> Literal #

SetRange TypedBindings # 
SetRange Pattern # 

Methods

setRange :: Range -> Pattern -> Pattern #

SetRange AbstractName # 
SetRange ConPatInfo # 
SetRange DeclInfo # 

Methods

setRange :: Range -> DeclInfo -> DeclInfo #

SetRange DefInfo # 

Methods

setRange :: Range -> DefInfo -> DefInfo #

SetRange ModuleInfo # 
SetRange ConHead # 

Methods

setRange :: Range -> ConHead -> ConHead #

SetRange MetaInfo # 

Methods

setRange :: Range -> MetaInfo -> MetaInfo #

SetRange MetaVariable # 
SetRange a => SetRange [a] # 

Methods

setRange :: Range -> [a] -> [a] #

SetRange a => SetRange (PrintRange a) # 

Methods

setRange :: Range -> PrintRange a -> PrintRange a #

SetRange a => SetRange (Arg a) # 

Methods

setRange :: Range -> Arg a -> Arg a #

SetRange a => SetRange (WithHiding a) # 

Methods

setRange :: Range -> WithHiding a -> WithHiding a #

SetRange (Pattern' a) # 

Methods

setRange :: Range -> Pattern' a -> Pattern' a #

SetRange a => SetRange (Named name a) # 

Methods

setRange :: Range -> Named name a -> Named name a #

class KillRange a where #

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

Minimal complete definition

killRange

Methods

killRange :: KillRangeT a #

Instances

KillRange Bool # 
KillRange Int # 
KillRange Integer # 
KillRange () # 

Methods

killRange :: KillRangeT () #

KillRange Void # 
KillRange String #

Overlaps with KillRange [a].

KillRange Range # 
KillRange Permutation # 
KillRange Fixity' # 
KillRange InteractionId # 
KillRange NameId # 
KillRange IsMacro # 
KillRange IsInstance # 
KillRange IsAbstract # 
KillRange Access # 
KillRange ProjOrigin # 
KillRange ConOrigin # 
KillRange ArgInfo # 
KillRange Origin # 
KillRange Relevance # 
KillRange Hiding # 
KillRange Induction # 
KillRange Delayed # 
KillRange QName # 
KillRange Name # 
KillRange GenPart # 
KillRange AmbiguousQName # 
KillRange ModuleName # 
KillRange QName # 
KillRange Name # 
KillRange Fixity # 
KillRange Literal # 
KillRange Compiled # 
KillRange Occurrence # 
KillRange Pragma # 
KillRange ModuleApplication # 
KillRange Declaration # 
KillRange AsName # 
KillRange WhereClause # 
KillRange RHS # 
KillRange LHS # 
KillRange TypedBinding # 
KillRange BoundName # 
KillRange TypedBindings # 
KillRange LamBinding # 
KillRange Pattern # 
KillRange Expr # 
KillRange ModuleAssignment # 
KillRange ScopeInfo # 
KillRange ConPatInfo # 
KillRange PatInfo # 
KillRange LHSInfo # 
KillRange MutualInfo # 
KillRange DeclInfo # 
KillRange DefInfo # 
KillRange LetInfo # 
KillRange ModuleInfo # 
KillRange ExprInfo # 
KillRange MetaInfo # 
KillRange Substitution # 
KillRange ConPatternInfo # 
KillRange DBPatVar # 
KillRange Clause # 
KillRange LevelAtom # 
KillRange PlusLevel # 
KillRange Level # 
KillRange Sort # 
KillRange Term # 
KillRange ConHead # 
KillRange LHS # 
KillRange SpineLHS # 
KillRange RHS # 
KillRange NamedDotPattern # 
KillRange TypedBinding # 
KillRange TypedBindings # 
KillRange LamBinding # 
KillRange LetBinding # 
KillRange ModuleApplication # 
KillRange Declaration # 
KillRange ScopeCopyInfo # 
KillRange Expr # 
KillRange CompiledClauses # 
KillRange CtxId # 
KillRange MutualId # 
KillRange TermHead # 
KillRange Defn # 
KillRange FunctionFlag # 
KillRange EtaEquality # 
KillRange ProjLams # 
KillRange Projection # 
KillRange ExtLamInfo # 
KillRange CompiledRepresentation # 
KillRange Polarity # 
KillRange Definition # 
KillRange RewriteRule # 
KillRange NLPType # 
KillRange NLPat # 
KillRange DisplayTerm # 
KillRange DisplayForm # 
KillRange Section # 
KillRange RewriteRuleMap # 
KillRange Definitions # 
KillRange Sections # 
KillRange Signature # 
KillRange a => KillRange [a] # 

Methods

killRange :: KillRangeT [a] #

KillRange a => KillRange (Maybe a) # 

Methods

killRange :: KillRangeT (Maybe a) #

(Ord a, KillRange a) => KillRange (Set a) # 

Methods

killRange :: KillRangeT (Set a) #

KillRange a => KillRange (PrintRange a) # 
KillRange a => KillRange (Drop a) # 

Methods

killRange :: KillRangeT (Drop a) #

KillRange m => KillRange (TerminationCheck m) # 
KillRange a => KillRange (MaybePlaceholder a) # 
KillRange (Ranged a) # 
KillRange a => KillRange (Dom a) # 

Methods

killRange :: KillRangeT (Dom a) #

KillRange a => KillRange (Arg a) # 

Methods

killRange :: KillRangeT (Arg a) #

KillRange a => KillRange (WithHiding a) # 
KillRange x => KillRange (ThingWithFixity x) # 
KillRange a => KillRange (FieldAssignment' a) # 
KillRange e => KillRange (OpApp e) # 

Methods

killRange :: KillRangeT (OpApp e) #

KillRange a => KillRange (Pattern' a) # 
KillRange a => KillRange (Blocked a) # 
KillRange a => KillRange (Tele a) # 

Methods

killRange :: KillRangeT (Tele a) #

KillRange a => KillRange (Type' a) # 

Methods

killRange :: KillRangeT (Type' a) #

KillRange a => KillRange (Abs a) # 

Methods

killRange :: KillRangeT (Abs a) #

KillRange a => KillRange (Elim' a) # 

Methods

killRange :: KillRangeT (Elim' a) #

KillRange e => KillRange (Pattern' e) # 
KillRange e => KillRange (LHSCore' e) # 
KillRange a => KillRange (Clause' a) # 
KillRange c => KillRange (Case c) # 

Methods

killRange :: KillRangeT (Case c) #

KillRange c => KillRange (WithArity c) # 
KillRange c => KillRange (FunctionInverse' c) # 
KillRange a => KillRange (Local a) # 

Methods

killRange :: KillRangeT (Local a) #

KillRange a => KillRange (Open a) # 

Methods

killRange :: KillRangeT (Open a) #

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

Methods

killRange :: KillRangeT (Either a b) #

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

Methods

killRange :: KillRangeT (a, b) #

KillRange a => KillRange (Map k a) # 

Methods

killRange :: KillRangeT (Map k a) #

(KillRange a, KillRange b) => KillRange (Renaming' a b) # 
(KillRange a, KillRange b) => KillRange (ImportedName' a b) # 
(KillRange a, KillRange b) => KillRange (Using' a b) # 

Methods

killRange :: KillRangeT (Using' a b) #

(KillRange a, KillRange b) => KillRange (ImportDirective' a b) # 
(KillRange name, KillRange a) => KillRange (Named name a) # 

Methods

killRange :: KillRangeT (Named name a) #

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

Methods

killRange :: KillRangeT (a, b, c) #

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

Methods

killRange :: KillRangeT (a, b, c, d) #

type KillRangeT a = a -> a #

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

Remove ranges in keys and values of a map.

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 #

Precondition: The ranges must point to the same file (or be empty).

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

Precondition: The ranges must point to the same file (or be empty).

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.

interleaveRanges :: HasRange a => [a] -> [a] -> ([a], [(a, a)]) #

Interleaves two streams of ranged elements

It will report the conflicts as a list of conflicting pairs. In case of conflict, the element with the earliest start position is placed first. In case of a tie, the element with the earliest ending position is placed first. If both tie, the element from the first list is placed first.