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

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

Instances

Functor Position' Source # 

Methods

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

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

Show PositionWithoutFile Source # 
Foldable Position' Source # 

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

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 Source # 
Eq a => Eq (Position' a) Source # 

Methods

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

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

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

Associated Types

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

Methods

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

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

Arbitrary a => Arbitrary (Position' a) Source # 

Methods

arbitrary :: Gen (Position' a) #

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

CoArbitrary a => CoArbitrary (Position' a) Source # 

Methods

coarbitrary :: Position' a -> Gen b -> Gen b #

Pretty a => Pretty (Position' (Maybe a)) Source # 
type Rep (Position' a) 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

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

Instances

Functor Interval' Source # 

Methods

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

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

Show IntervalWithoutFile Source # 
Foldable Interval' Source # 

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

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 Source # 
HasRange Interval Source # 
Eq a => Eq (Interval' a) Source # 

Methods

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

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

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

Associated Types

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

Methods

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

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

(Arbitrary a, Ord a) => Arbitrary (Interval' a) Source # 

Methods

arbitrary :: Gen (Interval' a) #

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

CoArbitrary a => CoArbitrary (Interval' a) Source # 

Methods

coarbitrary :: Interval' a -> Gen b -> Gen b #

Pretty a => Pretty (Interval' (Maybe a)) Source # 
type Rep (Interval' a) Source # 
type Rep (Interval' a) = D1 (MetaData "Interval'" "Agda.Syntax.Position" "Agda-2.5.1.2-3WdVW2PMESgFNbFxv8zcP5" 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 Source #

Converts a file name and two positions to an interval.

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

data Range' a Source #

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.

Instances

Functor Range' Source # 

Methods

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

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

Foldable Range' Source # 

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

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 Source # 
SetRange Range Source # 

Methods

setRange :: Range -> Range -> Range Source #

HasRange Range Source # 

Methods

getRange :: Range -> Range Source #

FreshName Range Source # 
GenC Range Source # 
PrettyTCM Range Source # 

Methods

prettyTCM :: Range -> TCM Doc Source #

Eq a => Eq (Range' a) Source # 

Methods

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

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

Ord a => Ord (Range' a) Source # 

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 (Range' Integer) Source # 
Show a => Show (Range' (Maybe a)) Source # 

Methods

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

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

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

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

Methods

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

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

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

Generic (Range' a) Source # 

Associated Types

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

Methods

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

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

(Ord a, Arbitrary a) => Arbitrary (Range' a) Source # 

Methods

arbitrary :: Gen (Range' a) #

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

CoArbitrary a => CoArbitrary (Range' a) Source # 

Methods

coarbitrary :: Range' a -> Gen b -> Gen b #

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

Methods

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

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

Null (Range' a) Source # 

Methods

empty :: Range' a Source #

null :: Range' a -> Bool Source #

FreshName (Range, String) Source # 
type Rep (Range' a) Source # 
type Rep (Range' a) = D1 (MetaData "Range'" "Agda.Syntax.Position" "Agda-2.5.1.2-3WdVW2PMESgFNbFxv8zcP5" False) ((:+:) (C1 (MetaCons "NoRange" PrefixI False) U1) (C1 (MetaCons "Range" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 a)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Seq IntervalWithoutFile))))))

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

Range invariant.

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

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

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

Precondition: consecutiveAndSeparated.

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

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

rangeFile :: Range -> SrcFile Source #

The file the range is pointing to.

rightMargin :: Range -> Range Source #

Conflate a range to its right margin.

noRange :: Range' a Source #

Ranges between two unknown positions

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

Converts two positions to a range.

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

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

Converts a file name and two positions to a range.

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

The initial position in the range, if any.

rStart' :: Range' a -> Maybe PositionWithoutFile 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.

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

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

rangeToInterval :: Range' a -> Maybe IntervalWithoutFile Source #

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

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 

class HasRange t where Source #

Things that have a range are instances of this class.

Minimal complete definition

getRange

Methods

getRange :: t -> Range Source #

Instances

HasRange Bool Source # 

Methods

getRange :: Bool -> Range Source #

HasRange Range Source # 

Methods

getRange :: Range -> Range Source #

HasRange Interval Source # 
HasRange ParseError Source # 
HasRange IsMacro Source # 
HasRange IsInstance Source # 
HasRange Induction Source # 
HasRange QName Source # 

Methods

getRange :: QName -> Range Source #

HasRange Name Source # 

Methods

getRange :: Name -> Range 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 # 

Methods

getRange :: QName -> Range Source #

HasRange Name Source # 

Methods

getRange :: Name -> Range Source #

HasRange Fixity Source # 
HasRange Literal Source # 
HasRange Pragma Source # 
HasRange ModuleApplication Source # 
HasRange Declaration Source # 
HasRange AsName Source # 
HasRange WhereClause Source # 
HasRange RHS Source # 

Methods

getRange :: RHS -> Range Source #

HasRange LHSCore Source # 
HasRange LHS Source # 

Methods

getRange :: LHS -> Range Source #

HasRange TypedBinding Source # 
HasRange BoundName Source # 
HasRange TypedBindings Source # 
HasRange LamBinding Source # 
HasRange Pattern Source # 
HasRange Expr Source # 

Methods

getRange :: Expr -> Range Source #

HasRange ModuleAssignment Source # 
HasRange DeclarationException Source # 
HasRange NiceDeclaration Source # 
HasRange Token Source # 

Methods

getRange :: Token -> Range 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 LHS Source # 

Methods

getRange :: LHS -> Range Source #

HasRange SpineLHS Source # 
HasRange RHS Source # 

Methods

getRange :: RHS -> Range Source #

HasRange TypedBinding Source # 
HasRange TypedBindings Source # 
HasRange LamBinding Source # 
HasRange LetBinding Source # 
HasRange Declaration Source # 
HasRange Expr Source # 

Methods

getRange :: Expr -> Range Source #

HasRange Clause Source # 
HasRange ConHead Source # 
HasRange TCErr Source # 

Methods

getRange :: TCErr -> Range Source #

HasRange Call Source # 

Methods

getRange :: Call -> Range Source #

HasRange MetaInfo Source # 
HasRange MetaVariable Source # 
HasRange Constraint Source # 
HasRange ProblemConstraint Source # 
HasRange a => HasRange [a] Source #

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

Methods

getRange :: [a] -> Range Source #

HasRange a => HasRange (Maybe a) Source # 

Methods

getRange :: Maybe a -> Range Source #

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

Methods

getRange :: Ranged a -> Range Source #

HasRange a => HasRange (Dom a) Source # 

Methods

getRange :: Dom a -> Range Source #

HasRange a => HasRange (Arg a) Source # 

Methods

getRange :: Arg a -> Range Source #

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

Methods

getRange :: OpApp e -> Range Source #

IsExpr e => HasRange (ExprView e) Source # 

Methods

getRange :: ExprView e -> Range Source #

HasRange (Pattern' e) Source # 

Methods

getRange :: Pattern' e -> Range Source #

HasRange (LHSCore' e) Source # 

Methods

getRange :: LHSCore' e -> Range Source #

HasRange a => HasRange (Clause' a) Source # 

Methods

getRange :: Clause' a -> Range Source #

HasRange a => HasRange (Closure a) Source # 

Methods

getRange :: Closure a -> Range Source #

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

Methods

getRange :: Either a b -> Range Source #

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

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

Methods

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

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

Methods

getRange :: Renaming' a b -> Range Source #

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

Methods

getRange :: Using' a b -> Range Source #

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

Methods

getRange :: Named name a -> Range Source #

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

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

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

Minimal complete definition

setRange

Methods

setRange :: Range -> t -> t Source #

Instances

SetRange Range Source # 

Methods

setRange :: Range -> Range -> Range Source #

SetRange QName Source # 

Methods

setRange :: Range -> QName -> QName Source #

SetRange Name Source # 

Methods

setRange :: Range -> Name -> Name Source #

SetRange ModuleName Source # 
SetRange QName Source # 

Methods

setRange :: Range -> QName -> QName Source #

SetRange Name Source # 

Methods

setRange :: Range -> Name -> Name Source #

SetRange Literal Source # 
SetRange TypedBindings Source # 
SetRange Pattern Source # 
SetRange AbstractName Source # 
SetRange ConPatInfo Source # 
SetRange DeclInfo Source # 
SetRange DefInfo Source # 
SetRange ModuleInfo Source # 
SetRange ConHead Source # 
SetRange MetaInfo Source # 
SetRange MetaVariable Source # 
SetRange a => SetRange [a] Source # 

Methods

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

SetRange a => SetRange (PrintRange a) Source # 
SetRange a => SetRange (Arg a) Source # 

Methods

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

SetRange a => SetRange (WithHiding a) Source # 
SetRange (Pattern' a) Source # 

Methods

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

SetRange a => SetRange (Named name a) Source # 

Methods

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

class KillRange a where Source #

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

Minimal complete definition

killRange

Instances

KillRange Bool Source # 
KillRange Int Source # 
KillRange Integer Source # 
KillRange () Source # 
KillRange Void Source # 
KillRange String Source #

Overlaps with KillRange [a].

KillRange Range Source # 
KillRange Occurrence Source # 
KillRange Permutation Source # 
KillRange Fixity' Source # 
KillRange InteractionId Source # 
KillRange NameId Source # 
KillRange IsMacro Source # 
KillRange IsInstance Source # 
KillRange IsAbstract Source # 
KillRange ArgInfo Source # 
KillRange Relevance Source # 
KillRange Hiding Source # 
KillRange Induction Source # 
KillRange Delayed Source # 
KillRange QName Source # 
KillRange Name Source # 
KillRange GenPart Source # 
KillRange AmbiguousQName Source # 
KillRange ModuleName Source # 
KillRange QName Source # 
KillRange Name Source # 
KillRange Fixity Source # 
KillRange Literal Source # 
KillRange Pragma Source # 
KillRange ModuleApplication Source # 
KillRange Declaration Source # 
KillRange AsName 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 ModuleAssignment Source # 
KillRange Compiled 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 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 Substitution Source # 
KillRange ConPatternInfo 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 CtxId Source # 
KillRange MutualId Source # 
KillRange TermHead Source # 
KillRange Defn Source # 
KillRange EtaEquality 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 a => KillRange (Drop a) Source # 
KillRange m => KillRange (TerminationCheck m) Source # 
KillRange a => KillRange (MaybePlaceholder a) Source # 
KillRange (Ranged a) Source # 
KillRange a => KillRange (Dom a) Source # 
KillRange a => KillRange (Arg a) Source # 
KillRange a => KillRange (WithHiding a) Source # 
KillRange x => KillRange (ThingWithFixity x) Source # 
KillRange a => KillRange (FieldAssignment' a) 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 (Pattern' 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 # 

Methods

killRange :: KillRangeT (a, b) Source #

KillRange a => KillRange (Map k a) Source # 

Methods

killRange :: KillRangeT (Map k a) Source #

(KillRange a, KillRange b) => KillRange (Renaming' a b) Source # 
(KillRange a, KillRange b) => KillRange (ImportedName' a b) Source # 
(KillRange a, KillRange b) => KillRange (Using' a b) Source # 
(KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source # 
(KillRange name, KillRange a) => KillRange (Named name a) Source # 

Methods

killRange :: KillRangeT (Named name a) Source #

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

Methods

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

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

Methods

killRange :: KillRangeT (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 #

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

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

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

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.