Agda-2.6.2.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Position

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

Instances details
Functor Position' Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

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

Foldable Position' Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

foldMap :: Monoid m => (a -> m) -> Position' a -> 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 # 
Instance details

Defined in Agda.Syntax.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) #

NFData PositionWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

rnf :: PositionWithoutFile -> () #

NFData Position Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

rnf :: Position -> () #

Pretty PositionWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

Eq a => Eq (Position' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

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

Data a => Data (Position' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Position' a -> c (Position' a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Position' a) #

toConstr :: Position' a -> Constr #

dataTypeOf :: Position' a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Position' a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Position' a)) #

gmapT :: (forall b. Data b => b -> b) -> Position' a -> Position' a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Position' a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Position' a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Position' a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Position' a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Position' a -> m (Position' a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Position' a -> m (Position' a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Position' a -> m (Position' a) #

Ord a => Ord (Position' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Read a => Read (Position' a) Source # 
Instance details

Defined in Agda.Interaction.Base

Show a => Show (Position' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Generic (Position' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Associated Types

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

Methods

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

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

ToJSON (Position' ()) Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Pretty a => Pretty (Position' (Maybe a)) Source # 
Instance details

Defined in Agda.Syntax.Position

EmbPrj a => EmbPrj (Position' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EncodeTCM (Position' ()) Source # 
Instance details

Defined in Agda.Interaction.JSONTop

type Rep (Position' a) Source # 
Instance details

Defined in Agda.Syntax.Position

type Rep (Position' a) = D1 ('MetaData "Position'" "Agda.Syntax.Position" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" 'False) (C1 ('MetaCons "Pn" 'PrefixI 'True) ((S1 ('MetaSel ('Just "srcFile") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a) :*: S1 ('MetaSel ('Just "posPos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int32)) :*: (S1 ('MetaSel ('Just "posLine") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int32) :*: S1 ('MetaSel ('Just "posCol") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int32))))

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

startPos' :: a -> Position' a Source #

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

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

Instances details
Functor Interval' Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

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

Foldable Interval' Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

foldMap :: Monoid m => (a -> m) -> Interval' a -> 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 # 
Instance details

Defined in Agda.Syntax.Position

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

NFData IntervalWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

rnf :: IntervalWithoutFile -> () #

NFData Interval Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

rnf :: Interval -> () #

Pretty IntervalWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

HasRange Interval Source # 
Instance details

Defined in Agda.Syntax.Position

Eq a => Eq (Interval' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

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

Data a => Data (Interval' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Interval' a -> c (Interval' a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Interval' a) #

toConstr :: Interval' a -> Constr #

dataTypeOf :: Interval' a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Interval' a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Interval' a)) #

gmapT :: (forall b. Data b => b -> b) -> Interval' a -> Interval' a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Interval' a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Interval' a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Interval' a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Interval' a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Interval' a -> m (Interval' a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Interval' a -> m (Interval' a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Interval' a -> m (Interval' a) #

Ord a => Ord (Interval' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Read a => Read (Interval' a) Source # 
Instance details

Defined in Agda.Interaction.Base

Show a => Show (Interval' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Generic (Interval' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Associated Types

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

Methods

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

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

Pretty a => Pretty (Interval' (Maybe a)) Source # 
Instance details

Defined in Agda.Syntax.Position

EmbPrj a => EmbPrj (Interval' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

type Rep (Interval' a) Source # 
Instance details

Defined in Agda.Syntax.Position

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

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

Converts a file name and two positions to an interval.

getIntervalFile :: Interval' a -> a Source #

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

iLength :: Interval' a -> Int32 Source #

The length of an interval.

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

Finds the least interval which covers the arguments.

Precondition: The intervals must point to the same file.

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

Sets the srcFile components of 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.

Constructors

NoRange 
Range !a (Seq IntervalWithoutFile) 

Instances

Instances details
Functor Range' Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

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

Foldable Range' Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

foldMap :: Monoid m => (a -> m) -> Range' a -> 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 # 
Instance details

Defined in Agda.Syntax.Position

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

ToJSON Range Source # 
Instance details

Defined in Agda.Interaction.JSONTop

KillRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

SetRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

HasRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Range -> Range Source #

Subst Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Range Source #

FreshName Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Range Source #

Ranges are always deserialised as noRange.

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

PrettyTCM Range Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Range -> m Doc Source #

EncodeTCM Range Source # 
Instance details

Defined in Agda.Interaction.JSONTop

LensClosure Range MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensClosure Range MetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.Syntax.Position

Methods

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

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

Data a => Data (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Range' a -> c (Range' a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Range' a) #

toConstr :: Range' a -> Constr #

dataTypeOf :: Range' a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Range' a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Range' a)) #

gmapT :: (forall b. Data b => b -> b) -> Range' a -> Range' a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Range' a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Range' a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Range' a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Range' a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Range' a -> m (Range' a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Range' a -> m (Range' a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Range' a -> m (Range' a) #

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

Defined in Agda.Syntax.Position

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 #

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

Note that the grammar implemented by this instance does not necessarily match the current representation of ranges.

Instance details

Defined in Agda.Interaction.Base

Show a => Show (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> Range' a -> ShowS #

show :: Range' a -> String #

showList :: [Range' a] -> ShowS #

Generic (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Associated Types

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

Methods

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

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

Semigroup a => Semigroup (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

sconcat :: NonEmpty (Range' a) -> Range' a #

stimes :: Integral b => b -> Range' a -> Range' a #

Semigroup a => Monoid (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

mempty :: Range' a #

mappend :: Range' a -> Range' a -> Range' a #

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

NFData a => NFData (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

rnf :: Range' a -> () #

Null (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

empty :: Range' a Source #

null :: Range' a -> Bool Source #

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

Defined in Agda.Syntax.Position

FreshName (Range, String) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type SubstArg Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type Rep (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

type Rep (Range' a) = D1 ('MetaData "Range'" "Agda.Syntax.Position" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" 'False) (C1 ('MetaCons "NoRange" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Range" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe 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.

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

Converts a file name and an interval to a range.

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.

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

Instances details
Eq a => Eq (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

(==) :: PrintRange a -> PrintRange a -> Bool #

(/=) :: PrintRange a -> PrintRange a -> Bool #

Ord a => Ord (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

(Pretty a, HasRange a) => Pretty (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange a => KillRange (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

SetRange a => SetRange (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

HasRange a => HasRange (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

class HasRange a where Source #

Things that have a range are instances of this class.

Minimal complete definition

Nothing

Methods

getRange :: a -> Range Source #

default getRange :: (Foldable t, HasRange b, t b ~ a) => a -> Range Source #

Instances

Instances details
HasRange Bool Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Bool -> Range Source #

HasRange () Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: () -> Range Source #

HasRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Range -> Range Source #

HasRange Interval Source # 
Instance details

Defined in Agda.Syntax.Position

HasRange GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Access Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Origin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Erased Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Modality Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Layer Source # 
Instance details

Defined in Agda.Syntax.Parser.Literate

Methods

getRange :: Layer -> Range Source #

HasRange TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

HasRange QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: QName -> Range Source #

HasRange Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: Name -> Range Source #

HasRange TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: TCErr -> Range Source #

HasRange AmbiguousQName Source #

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

Instance details

Defined in Agda.Syntax.Abstract.Name

HasRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

HasRange QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: QName -> Range Source #

HasRange Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: Name -> Range Source #

HasRange Token Source # 
Instance details

Defined in Agda.Syntax.Parser.Tokens

Methods

getRange :: Token -> Range Source #

HasRange ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

HasRange ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

HasRange Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: RHS -> Range Source #

HasRange LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: LHS -> Range Source #

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: Expr -> Range Source #

HasRange ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange NiceDeclaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

HasRange DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

HasRange DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

HasRange DeclarationException' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

HasRange DeclarationException Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

HasRange Attribute Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

HasRange AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

HasRange ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

HasRange ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

HasRange LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHS -> Range Source #

HasRange SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: RHS -> Range Source #

HasRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Expr -> Range Source #

HasRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange Call Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Call -> Range Source #

HasRange CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange MetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange Item Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

getRange :: Item -> Range Source #

HasRange HaskellPragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pragmas

HasRange a => HasRange [a] Source #

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

Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: [a] -> Range Source #

HasRange a => HasRange (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Maybe a -> Range Source #

HasRange a => HasRange (List1 a) Source #

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

Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: List1 a -> Range Source #

HasRange a => HasRange (List2 a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: List2 a -> Range Source #

HasRange a => HasRange (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

HasRange a => HasRange (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Ranged a -> Range Source #

HasRange a => HasRange (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Arg a -> Range Source #

HasRange a => HasRange (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange a => HasRange (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange a => HasRange (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: HasEta' a -> Range Source #

HasRange a => HasRange (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange a => HasRange (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange e => HasRange (OpApp e) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: OpApp e -> Range Source #

IsExpr e => HasRange (ExprView e) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Operators.Parser

Methods

getRange :: ExprView e -> Range Source #

HasRange (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: DefInfo' t -> Range Source #

HasRange (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Pattern' e -> Range Source #

HasRange (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHSCore' e -> Range Source #

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

Defined in Agda.Syntax.Abstract

Methods

getRange :: Clause' a -> Range Source #

HasRange a => HasRange (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Binder' a -> Range Source #

HasRange a => HasRange (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Closure a -> Range Source #

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

Defined in Agda.Syntax.Position

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

Instance details

Defined in Agda.Syntax.Position

Methods

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

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

Defined in Agda.Syntax.Common

Methods

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

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

Methods

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

(HasRange a, HasRange b) => HasRange (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange a => HasRange (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Named name a -> Range Source #

HasRange a => HasRange (Dom' t a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getRange :: Dom' t 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).

Instance details

Defined in Agda.Syntax.Position

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

Instance details

Defined in Agda.Syntax.Position

Methods

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

(HasRange qn, HasRange nm, HasRange p, HasRange e) => HasRange (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: RewriteEqn' qn nm p e -> 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).

Instance details

Defined in Agda.Syntax.Position

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

Instance details

Defined in Agda.Syntax.Position

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

Instance details

Defined in Agda.Syntax.Position

Methods

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

class HasRange a => SetRange a 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

Nothing

Methods

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

default setRange :: (Functor f, SetRange b, f b ~ a) => Range -> a -> a Source #

Instances

Instances details
SetRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

SetRange GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

SetRange QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

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

SetRange Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

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

SetRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

SetRange QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

SetRange Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

SetRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange Attribute Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

SetRange AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

SetRange ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

SetRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

SetRange MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

SetRange MetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

SetRange a => SetRange [a] Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

SetRange a => SetRange (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

SetRange a => SetRange (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

SetRange a => SetRange (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

SetRange a => SetRange (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange a => SetRange (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

SetRange (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

Defined in Agda.Syntax.Common

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

Nothing

Methods

killRange :: KillRangeT a Source #

default killRange :: (Functor f, KillRange b, f b ~ a) => KillRangeT a Source #

Instances

Instances details
KillRange Bool Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange Int Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange Integer Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange () Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange String Source #

Overlaps with KillRange [a].

Instance details

Defined in Agda.Syntax.Position

KillRange Void Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange Permutation Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange Range Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange NameId Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Access Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Origin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Erased Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Modality Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Language Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

KillRange QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

KillRange Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

KillRange Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Suffix Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange Literal Source # 
Instance details

Defined in Agda.Syntax.Literal

KillRange Compiled Source # 
Instance details

Defined in Agda.Syntax.Treeless

KillRange Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

KillRange Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

KillRange Attribute Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

KillRange ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

KillRange ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange Substitution Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange ConPatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange PatOrigin Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange PatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Level Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Term Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

KillRange LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Projection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange System Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange CompiledRepresentation Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange RewriteRuleMap Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Definitions Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Sections Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Signature Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange a => KillRange [a] Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange a => KillRange (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Position

(Ord a, KillRange a) => KillRange (Set a) Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange a => KillRange (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange a => KillRange (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange a => KillRange (Drop a) Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange a => KillRange (List2 a) Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange a => KillRange (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange m => KillRange (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange a => KillRange (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange a => KillRange (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange a => KillRange (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange a => KillRange (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange a => KillRange (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange a => KillRange (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange x => KillRange (ThingWithFixity x) Source # 
Instance details

Defined in Agda.Syntax.Fixity

KillRange a => KillRange (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange e => KillRange (OpApp e) Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange a => KillRange (SplitTree' a) Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

KillRange t => KillRange (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange a => KillRange (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Elim

KillRange a => KillRange (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange a => KillRange (Blocked a) Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange a => KillRange (Tele a) Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange a => KillRange (Type' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange a => KillRange (Abs a) Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange c => KillRange (Case c) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

KillRange c => KillRange (WithArity c) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

KillRange e => KillRange (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange e => KillRange (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange a => KillRange (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange a => KillRange (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange c => KillRange (FunctionInverse' c) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange a => KillRange (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange a => KillRange (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

(KillRange a, KillRange b) => KillRange (Either a b) Source # 
Instance details

Defined in Agda.Syntax.Position

(KillRange a, KillRange b) => KillRange (a, b) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (a, b) Source #

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

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Map k a) Source #

(KillRange a, KillRange b) => KillRange (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(KillRange a, KillRange b) => KillRange (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(KillRange a, KillRange b) => KillRange (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(KillRange name, KillRange a) => KillRange (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Named name a) Source #

(KillRange t, KillRange a) => KillRange (Dom' t a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Dom' t a) Source #

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

Defined in Agda.Syntax.Position

Methods

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

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

Defined in Agda.Syntax.Position

Methods

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

(KillRange qn, KillRange nm, KillRange e, KillRange p) => KillRange (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (RewriteEqn' qn nm p e) 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.

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

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.

Orphan instances