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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Position

Contents

- Positions
- Intervals
- Ranges

Description

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

Synopsis

- type Position = Position' SrcFile
- type PositionWithoutFile = Position' ()
- data Position' a = Pn {
  - srcFile :: !a
  - posPos :: !Word32
  - posLine :: !Word32
  - posCol :: !Word32
  }
- type SrcFile = Maybe RangeFile
- data RangeFile = RangeFile {
  - rangeFilePath :: !AbsolutePath
  - rangeFileName :: !(Maybe (TopLevelModuleName' Range))
  }
- mkRangeFile :: AbsolutePath -> Maybe (TopLevelModuleName' Range) -> RangeFile
- positionInvariant :: Position' a -> Bool
- startPos :: Maybe RangeFile -> Position
- startPos' :: a -> Position' a
- movePos :: Position' a -> Char -> Position' a
- movePosByString :: Foldable t => Position' a -> t Char -> Position' a
- backupPos :: Position' a -> Position' a
- type Interval = Interval' SrcFile
- type IntervalWithoutFile = Interval' ()
- data Interval' a = Interval a !PositionWithoutFile !PositionWithoutFile
- intervalInvariant :: Ord a => Interval' a -> Bool
- iStart :: Interval' a -> Position' a
- iEnd :: Interval' a -> Position' a
- posToInterval :: a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
- getIntervalFile :: Interval' a -> a
- iLength :: Interval' a -> Word32
- fuseIntervals :: IntervalWithoutFile -> IntervalWithoutFile -> IntervalWithoutFile
- type Range = Range' SrcFile
- type RangeWithoutFile = Range' ()
- data Range' a
  - = NoRange
  - | Range !a (Seq IntervalWithoutFile)
- rangeInvariant :: Ord a => Range' a -> Bool
- consecutiveAndSeparated :: Ord a => [Interval' a] -> Bool
- intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a
- intervalToRange :: a -> IntervalWithoutFile -> Range' a
- rangeFromAbsolutePath :: AbsolutePath -> Range
- rangeIntervals :: Range' a -> [IntervalWithoutFile]
- rangeFile :: Range -> SrcFile
- rangeModule' :: Range -> Maybe (Maybe (TopLevelModuleName' Range))
- rangeModule :: Range -> Maybe (TopLevelModuleName' Range)
- rightMargin :: Range -> Range
- noRange :: Range' a
- posToRange :: Position' a -> Position' a -> Range' a
- posToRange' :: a -> PositionWithoutFile -> PositionWithoutFile -> Range' a
- rStart :: Range' a -> Maybe (Position' a)
- rStart' :: Range' a -> Maybe PositionWithoutFile
- rEnd :: Range' a -> Maybe (Position' a)
- rEnd' :: Range' a -> Maybe PositionWithoutFile
- rangeToInterval :: Range' a -> Maybe IntervalWithoutFile
- rangeToIntervalWithFile :: Range' a -> Maybe (Interval' a)
- continuous :: Range' a -> Range' a
- continuousPerLine :: Ord a => Range' a -> Range' a
- newtype PrintRange a = PrintRange a
- class HasRange a where
  - getRange :: a -> Range
- class HasRangeWithoutFile a where
  - getRangeWithoutFile :: a -> RangeWithoutFile
- class HasRange a => SetRange a where
  - setRange :: Range -> a -> a
- class KillRange a where
  - killRange :: KillRangeT a
- type KillRangeT a = a -> a
- killRangeMap :: (KillRange k, KillRange v) => KillRangeT (Map k v)
- class KILLRANGE t (b :: Bool) where
  - killRangeN :: t -> t
- withRangeOf :: (SetRange t, HasRange u) => t -> u -> t
- fuseRange :: (HasRange u, HasRange t) => u -> t -> Range
- fuseRanges :: Ord a => Range' a -> Range' a -> Range' a
- beginningOf :: Range -> Range
- beginningOfFile :: BeginningOfFile a => a -> Range
- interleaveRanges :: HasRangeWithoutFile a => [a] -> [a] -> ([a], [(a, a)])

# Positions

type Position = Position' SrcFile Source #

type PositionWithoutFile = Position' () Source #

data Position' a Source #

Represents a point in the input.

If two positions have the same `srcFile` and `posPos` components, then the final two components should be the same as well, but since this can be hard to enforce the program should not rely too much on the last two components; they are mainly there to improve error messages for the user.

Note the invariant which positions have to satisfy: `positionInvariant`.

Constructors

Pn |

Fields

- srcFile :: !a

  File.

- posPos :: !Word32

  Position, counting from 1.

- posLine :: !Word32

  Line number, counting from 1.

- posCol :: !Word32

  Column number, counting from 1.

#### Instances

Instances details

Pretty PositionWithoutFile Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: PositionWithoutFile -> Doc Source # prettyPrec :: Int -> PositionWithoutFile -> Doc Source # prettyList :: [PositionWithoutFile] -> Doc Source #
NFData Position Source # |
Instance details Defined in Agda.Syntax.Position Methods rnf :: Position -> () Source #
NFData PositionWithoutFile Source # |
Instance details Defined in Agda.Syntax.Position Methods rnf :: PositionWithoutFile -> () Source #
Functor Position' Source # |
Instance details Defined in Agda.Syntax.Position Methods fmap :: (a -> b) -> Position' a -> Position' b Source # (<$) :: a -> Position' b -> Position' a Source #
Foldable Position' Source # |

Instance details

Defined in Agda.Syntax.Position

Methods

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

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

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

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

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

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

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

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

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

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

null :: Position' a -> Bool Source #

length :: Position' a -> Int Source #

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

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

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

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

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

Traversable Position' Source # |
Instance details Defined in Agda.Syntax.Position Methods traverse :: Applicative f => (a -> f b) -> Position' a -> f (Position' b) Source # sequenceA :: Applicative f => Position' (f a) -> f (Position' a) Source # mapM :: Monad m => (a -> m b) -> Position' a -> m (Position' b) Source # sequence :: Monad m => Position' (m a) -> m (Position' a) Source #
EncodeTCM (Position' ()) Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Position' () -> TCM Value Source #
Pretty a => Pretty (Position' (Maybe a)) Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: Position' (Maybe a) -> Doc Source # prettyPrec :: Int -> Position' (Maybe a) -> Doc Source # prettyList :: [Position' (Maybe a)] -> Doc Source #
EmbPrj a => EmbPrj (Position' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Position' a -> S Word32 Source # icod_ :: Position' a -> S Word32 Source # value :: Word32 -> R (Position' a) Source #
ToJSON (Position' ()) Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: Position' () -> Value Source # toEncoding :: Position' () -> Encoding Source # toJSONList :: [Position' ()] -> Value Source # toEncodingList :: [Position' ()] -> Encoding Source # omitField :: Position' () -> Bool Source #
Generic (Position' a) Source # |

Instance details

Defined in Agda.Syntax.Position

Associated Types

type Rep (Position' a) |

Instance details

Defined in Agda.Syntax.Position

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

Methods

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

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

Read a => Read (Position' a) Source # |
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS (Position' a) Source # readList :: ReadS [Position' a] Source # readPrec :: ReadPrec (Position' a) Source # readListPrec :: ReadPrec [Position' a] Source #
Show a => Show (Position' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods showsPrec :: Int -> Position' a -> ShowS Source # show :: Position' a -> String Source # showList :: [Position' a] -> ShowS Source #
Eq a => Eq (Position' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods (==) :: Position' a -> Position' a -> Bool Source # (/=) :: Position' a -> Position' a -> Bool Source #
Ord a => Ord (Position' a) Source # |

Instance details

Defined in Agda.Syntax.Position

Methods

compare :: Position' a -> Position' a -> Ordering Source #

(<) :: Position' a -> Position' a -> Bool Source #

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

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

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

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

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

type Rep (Position' a) Source # |

Instance details

Defined in Agda.Syntax.Position

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

type SrcFile = Maybe RangeFile Source #

data RangeFile Source #

File information used in the `Position`, `Interval` and `Range` types.

Constructors

RangeFile |

Fields

- rangeFilePath :: !AbsolutePath

  The file's path.

- rangeFileName :: !(Maybe (TopLevelModuleName' Range))

  The file's top-level module name (if applicable).

  This field is optional, but some things may break if the field is not instantiated with an actual top-level module name. For instance, the `Eq` and `Ord` instances only make use of this field.

  The field uses `Maybe` rather than `Maybe` because it should be possible to instantiate it with something that is not yet defined (see `parseSource`).

  This '(TopLevelModuleName' Range)' should not contain a range.

#### Instances

Instances details

EncodeTCM Range Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Range -> TCM Value Source #
Pretty RangeFile Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: RangeFile -> Doc Source # prettyPrec :: Int -> RangeFile -> Doc Source # prettyList :: [RangeFile] -> Doc Source #
Pretty TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods pretty :: TopLevelModuleName -> Doc Source # prettyPrec :: Int -> TopLevelModuleName -> Doc Source # prettyList :: [TopLevelModuleName] -> Doc Source #
HasRange Interval Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: Interval -> Range Source #
HasRange Range Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: Range -> Range Source #
KillRange Range Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Range Source #
SetRange Range Source # |
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> Range -> Range Source #
FreshName Range Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => Range -> m Name Source #
PrettyTCM Range Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Range -> m Doc Source #
PrettyTCM TopLevelModuleName Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TopLevelModuleName -> m Doc Source #
EmbPrj Range Source # | Ranges are always deserialised as `noRange`.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Range -> S Word32 Source # icod_ :: Range -> S Word32 Source # value :: Word32 -> R Range Source #
EmbPrj RangeFile Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: RangeFile -> S Word32 Source # icod_ :: RangeFile -> S Word32 Source # value :: Word32 -> R RangeFile Source #
EmbPrj TopLevelModuleName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: TopLevelModuleName -> S Word32 Source # icod_ :: TopLevelModuleName -> S Word32 Source # value :: Word32 -> R TopLevelModuleName Source #
Subst Range Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Range |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Range = Term

Methods

applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source #

Sized TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods size :: TopLevelModuleName -> Int Source # natSize :: TopLevelModuleName -> Peano Source #
ToJSON Range Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: Range -> Value Source # toEncoding :: Range -> Encoding Source # toJSONList :: [Range] -> Value Source # toEncodingList :: [Range] -> Encoding Source # omitField :: Range -> Bool Source #
NFData Interval Source # |
Instance details Defined in Agda.Syntax.Position Methods rnf :: Interval -> () Source #
NFData Position Source # |
Instance details Defined in Agda.Syntax.Position Methods rnf :: Position -> () Source #
NFData RangeFile Source # |
Instance details Defined in Agda.Syntax.Position Methods rnf :: RangeFile -> () Source #
Generic RangeFile Source # |

Instance details

Defined in Agda.Syntax.Position

Associated Types

type Rep RangeFile |

Instance details

Defined in Agda.Syntax.Position

type Rep RangeFile = D1 ('MetaData "RangeFile" "Agda.Syntax.Position" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "RangeFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "rangeFilePath") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 AbsolutePath) :*: S1 ('MetaSel ('Just "rangeFileName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (TopLevelModuleName' Range)))))

Methods

from :: RangeFile -> Rep RangeFile x Source #

to :: Rep RangeFile x -> RangeFile Source #

Read RangeFile Source # | This instance fills in the `TopLevelModuleName`s using `Nothing`. Note that these occurrences of `Nothing` are "overwritten" by `parseIOTCM`.
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS RangeFile Source # readList :: ReadS [RangeFile] Source # readPrec :: ReadPrec RangeFile Source # readListPrec :: ReadPrec [RangeFile] Source #
Show RangeFile Source # |
Instance details Defined in Agda.Syntax.Position Methods showsPrec :: Int -> RangeFile -> ShowS Source # show :: RangeFile -> String Source # showList :: [RangeFile] -> ShowS Source #
Eq RangeFile Source # | Only the `rangeFileName` component is compared.
Instance details Defined in Agda.Syntax.Position Methods (==) :: RangeFile -> RangeFile -> Bool Source # (/=) :: RangeFile -> RangeFile -> Bool Source #
Ord RangeFile Source # | Only the `rangeFileName` component is compared.

Instance details

Defined in Agda.Syntax.Position

Methods

compare :: RangeFile -> RangeFile -> Ordering Source #

(<) :: RangeFile -> RangeFile -> Bool Source #

(<=) :: RangeFile -> RangeFile -> Bool Source #

(>) :: RangeFile -> RangeFile -> Bool Source #

(>=) :: RangeFile -> RangeFile -> Bool Source #

max :: RangeFile -> RangeFile -> RangeFile Source #

min :: RangeFile -> RangeFile -> RangeFile Source #

LensClosure MetaInfo Range Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lensClosure :: Lens' MetaInfo (Closure Range) Source #
LensClosure MetaVariable Range Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lensClosure :: Lens' MetaVariable (Closure Range) Source #
HasRange (TopLevelModuleName' Range) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: TopLevelModuleName' Range -> Range Source #
KillRange (TopLevelModuleName' Range) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (TopLevelModuleName' Range) Source #
SetRange (TopLevelModuleName' Range) Source # |
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> TopLevelModuleName' Range -> TopLevelModuleName' Range Source #
FreshName (Range, String) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => (Range, String) -> m Name Source #
type SubstArg Range Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Range = Term
type Rep RangeFile Source # |

Instance details

Defined in Agda.Syntax.Position

type Rep RangeFile = D1 ('MetaData "RangeFile" "Agda.Syntax.Position" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "RangeFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "rangeFilePath") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 AbsolutePath) :*: S1 ('MetaSel ('Just "rangeFileName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (TopLevelModuleName' Range)))))

mkRangeFile :: AbsolutePath -> Maybe (TopLevelModuleName' Range) -> RangeFile Source #

A smart constructor for `RangeFile`.

positionInvariant :: Position' a -> Bool Source #

startPos :: Maybe RangeFile -> Position Source #

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

startPos' :: a -> Position' a 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 :: Foldable t => Position' a -> t Char -> Position' a Source #

Advance the position by a string.

    movePosByString = foldl' movePos

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

Backup the position by one character.

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

# Intervals

type Interval = Interval' SrcFile Source #

type IntervalWithoutFile = Interval' () Source #

data Interval' a Source #

An interval. The `iEnd` position is not included in the interval.

Note the invariant which intervals have to satisfy: `intervalInvariant`.

Constructors

Interval a !PositionWithoutFile !PositionWithoutFile |

#### Instances

Instances details

Pretty IntervalWithoutFile Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: IntervalWithoutFile -> Doc Source # prettyPrec :: Int -> IntervalWithoutFile -> Doc Source # prettyList :: [IntervalWithoutFile] -> Doc Source #
HasRange Interval Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: Interval -> Range Source #
HasRangeWithoutFile IntervalWithoutFile Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: IntervalWithoutFile -> RangeWithoutFile Source #
NFData Interval Source # |
Instance details Defined in Agda.Syntax.Position Methods rnf :: Interval -> () Source #
NFData IntervalWithoutFile Source # |
Instance details Defined in Agda.Syntax.Position Methods rnf :: IntervalWithoutFile -> () Source #
Functor Interval' Source # |
Instance details Defined in Agda.Syntax.Position Methods fmap :: (a -> b) -> Interval' a -> Interval' b Source # (<$) :: a -> Interval' b -> Interval' a Source #
Foldable Interval' Source # |

Instance details

Defined in Agda.Syntax.Position

Methods

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

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

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

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

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

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

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

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

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

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

null :: Interval' a -> Bool Source #

length :: Interval' a -> Int Source #

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

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

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

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

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

Traversable Interval' Source # |
Instance details Defined in Agda.Syntax.Position Methods traverse :: Applicative f => (a -> f b) -> Interval' a -> f (Interval' b) Source # sequenceA :: Applicative f => Interval' (f a) -> f (Interval' a) Source # mapM :: Monad m => (a -> m b) -> Interval' a -> m (Interval' b) Source # sequence :: Monad m => Interval' (m a) -> m (Interval' a) Source #
Pretty a => Pretty (Interval' (Maybe a)) Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: Interval' (Maybe a) -> Doc Source # prettyPrec :: Int -> Interval' (Maybe a) -> Doc Source # prettyList :: [Interval' (Maybe a)] -> Doc Source #
EmbPrj a => EmbPrj (Interval' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Interval' a -> S Word32 Source # icod_ :: Interval' a -> S Word32 Source # value :: Word32 -> R (Interval' a) Source #
Generic (Interval' a) Source # |

Instance details

Defined in Agda.Syntax.Position

Associated Types

type Rep (Interval' a) |

Instance details

Defined in Agda.Syntax.Position

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

Methods

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

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

Read a => Read (Interval' a) Source # |
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS (Interval' a) Source # readList :: ReadS [Interval' a] Source # readPrec :: ReadPrec (Interval' a) Source # readListPrec :: ReadPrec [Interval' a] Source #
Show a => Show (Interval' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods showsPrec :: Int -> Interval' a -> ShowS Source # show :: Interval' a -> String Source # showList :: [Interval' a] -> ShowS Source #
Eq a => Eq (Interval' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods (==) :: Interval' a -> Interval' a -> Bool Source # (/=) :: Interval' a -> Interval' a -> Bool Source #
Ord a => Ord (Interval' a) Source # |

Instance details

Defined in Agda.Syntax.Position

Methods

compare :: Interval' a -> Interval' a -> Ordering Source #

(<) :: Interval' a -> Interval' a -> Bool Source #

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

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

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

max :: Interval' a -> Interval' a -> Interval' a Source #

min :: Interval' a -> Interval' a -> Interval' a Source #

type Rep (Interval' a) Source # |

Instance details

Defined in Agda.Syntax.Position

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

intervalInvariant :: Ord a => Interval' a -> Bool Source #

iStart :: Interval' a -> Position' a Source #

iEnd :: Interval' a -> Position' a Source #

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

Converts a file name and two positions to an interval. Sort the positions ascendingly.

getIntervalFile :: Interval' a -> a Source #

iLength :: Interval' a -> Word32 Source #

The length of an interval.

fuseIntervals :: IntervalWithoutFile -> IntervalWithoutFile -> IntervalWithoutFile Source #

Finds the least interval which covers the arguments.

# Ranges

type Range = Range' SrcFile Source #

type RangeWithoutFile = Range' () Source #

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

EncodeTCM Range Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Range -> TCM Value Source #
Pretty TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods pretty :: TopLevelModuleName -> Doc Source # prettyPrec :: Int -> TopLevelModuleName -> Doc Source # prettyList :: [TopLevelModuleName] -> Doc Source #
HasRange Range Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: Range -> Range Source #
HasRangeWithoutFile RangeWithoutFile Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: RangeWithoutFile -> RangeWithoutFile Source #
KillRange Range Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Range Source #
SetRange Range Source # |
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> Range -> Range Source #
FreshName Range Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => Range -> m Name Source #
PrettyTCM Range Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Range -> m Doc Source #
PrettyTCM TopLevelModuleName Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TopLevelModuleName -> m Doc Source #
EmbPrj Range Source # | Ranges are always deserialised as `noRange`.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Range -> S Word32 Source # icod_ :: Range -> S Word32 Source # value :: Word32 -> R Range Source #
EmbPrj TopLevelModuleName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: TopLevelModuleName -> S Word32 Source # icod_ :: TopLevelModuleName -> S Word32 Source # value :: Word32 -> R TopLevelModuleName Source #
Subst Range Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Range |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Range = Term

Methods

applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source #

Sized TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods size :: TopLevelModuleName -> Int Source # natSize :: TopLevelModuleName -> Peano Source #
ToJSON Range Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: Range -> Value Source # toEncoding :: Range -> Encoding Source # toJSONList :: [Range] -> Value Source # toEncodingList :: [Range] -> Encoding Source # omitField :: Range -> Bool Source #
Functor Range' Source # |
Instance details Defined in Agda.Syntax.Position Methods fmap :: (a -> b) -> Range' a -> Range' b Source # (<$) :: a -> Range' b -> Range' a Source #
Foldable Range' Source # |

Instance details

Defined in Agda.Syntax.Position

Methods

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

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

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

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

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

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

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

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

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

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

null :: Range' a -> Bool Source #

length :: Range' a -> Int Source #

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

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

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

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

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

Traversable Range' Source # |
Instance details Defined in Agda.Syntax.Position Methods traverse :: Applicative f => (a -> f b) -> Range' a -> f (Range' b) Source # sequenceA :: Applicative f => Range' (f a) -> f (Range' a) Source # mapM :: Monad m => (a -> m b) -> Range' a -> m (Range' b) Source # sequence :: Monad m => Range' (m a) -> m (Range' a) Source #
LensClosure MetaInfo Range Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lensClosure :: Lens' MetaInfo (Closure Range) Source #
LensClosure MetaVariable Range Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lensClosure :: Lens' MetaVariable (Closure Range) Source #
Pretty a => Pretty (Range' (Maybe a)) Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: Range' (Maybe a) -> Doc Source # prettyPrec :: Int -> Range' (Maybe a) -> Doc Source # prettyList :: [Range' (Maybe a)] -> Doc Source #
HasRange (TopLevelModuleName' Range) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: TopLevelModuleName' Range -> Range Source #
KillRange (TopLevelModuleName' Range) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (TopLevelModuleName' Range) Source #
SetRange (TopLevelModuleName' Range) Source # |
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> TopLevelModuleName' Range -> TopLevelModuleName' Range Source #
Null (Range' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods empty :: Range' a Source # null :: Range' a -> Bool Source #
NFData a => NFData (Range' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods rnf :: Range' a -> () Source #
Eq a => Monoid (Range' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods mempty :: Range' a Source # mappend :: Range' a -> Range' a -> Range' a Source # mconcat :: [Range' a] -> Range' a Source #
Eq a => Semigroup (Range' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods (<>) :: Range' a -> Range' a -> Range' a Source # sconcat :: NonEmpty (Range' a) -> Range' a Source # stimes :: Integral b => b -> Range' a -> Range' a Source #
Generic (Range' a) Source # |

Instance details

Defined in Agda.Syntax.Position

Associated Types

type Rep (Range' a) |

Instance details

Defined in Agda.Syntax.Position

type Rep (Range' a) = D1 ('MetaData "Range'" "Agda.Syntax.Position" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

Methods

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

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

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 Methods readsPrec :: Int -> ReadS (Range' a) Source # readList :: ReadS [Range' a] Source # readPrec :: ReadPrec (Range' a) Source # readListPrec :: ReadPrec [Range' a] Source #
Show a => Show (Range' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods showsPrec :: Int -> Range' a -> ShowS Source # show :: Range' a -> String Source # showList :: [Range' a] -> ShowS Source #
Eq a => Eq (Range' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods (==) :: Range' a -> Range' a -> Bool Source # (/=) :: Range' a -> Range' a -> Bool Source #
Ord a => Ord (Range' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods compare :: Range' a -> Range' a -> Ordering Source # (<) :: Range' a -> Range' a -> Bool Source # (<=) :: Range' a -> Range' a -> Bool Source # (>) :: Range' a -> Range' a -> Bool Source # (>=) :: Range' a -> Range' a -> Bool Source # max :: Range' a -> Range' a -> Range' a Source # min :: Range' a -> Range' a -> Range' a Source #
FreshName (Range, String) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => (Range, String) -> m Name Source #
type SubstArg Range Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Range = Term
type Rep (Range' a) Source # |

Instance details

Defined in Agda.Syntax.Position

type Rep (Range' a) = D1 ('MetaData "Range'" "Agda.Syntax.Position" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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.

rangeFromAbsolutePath :: AbsolutePath -> Range Source #

Range pointing to the first position in the given file.

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.

rangeModule' :: Range -> Maybe (Maybe (TopLevelModuleName' Range)) Source #

The range's top-level module name, if any.

If there is no range, then `Nothing` is returned. If there is a range without a module name, then ``Just` `Nothing`` is returned.

rangeModule :: Range -> Maybe (TopLevelModuleName' Range) Source #

The range's top-level module name, if any.

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

(Pretty a, HasRange a) => Pretty (PrintRange a) Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: PrintRange a -> Doc Source # prettyPrec :: Int -> PrintRange a -> Doc Source # prettyList :: [PrintRange a] -> Doc Source #
HasRange a => HasRange (PrintRange a) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: PrintRange a -> Range Source #
KillRange a => KillRange (PrintRange a) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (PrintRange a) Source #
SetRange a => SetRange (PrintRange a) Source # |
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> PrintRange a -> PrintRange a Source #
Eq a => Eq (PrintRange a) Source # |
Instance details Defined in Agda.Syntax.Position Methods (==) :: PrintRange a -> PrintRange a -> Bool Source # (/=) :: PrintRange a -> PrintRange a -> Bool Source #
Ord a => Ord (PrintRange a) Source # |

Instance details

Defined in Agda.Syntax.Position

Methods

compare :: PrintRange a -> PrintRange a -> Ordering Source #

(<) :: PrintRange a -> PrintRange a -> Bool Source #

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

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

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

max :: PrintRange a -> PrintRange a -> PrintRange a Source #

min :: PrintRange a -> PrintRange a -> PrintRange a Source #

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 :: forall (t :: Type -> Type) b. (Foldable t, HasRange b, t b ~ a) => a -> Range Source #

#### Instances

Instances details

HasRange HaskellPragma Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pragmas Methods getRange :: HaskellPragma -> Range Source #
HasRange BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: BindName -> Range Source #
HasRange Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Declaration -> Range Source #
HasRange Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Expr -> Range Source #
HasRange LHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LHS -> Range Source #
HasRange LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LamBinding -> Range Source #
HasRange LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LetBinding -> Range Source #
HasRange RHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: RHS -> Range Source #
HasRange SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: SpineLHS -> Range Source #
HasRange TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: TypedBinding -> Range Source #
HasRange WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: WhereDeclarations -> 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 Methods getRange :: AmbiguousQName -> Range Source #
HasRange ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: ModuleName -> Range Source #
HasRange Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: Name -> Range Source #
HasRange QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: QName -> Range Source #
HasRange Access Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Access -> Range Source #
HasRange Annotation Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Annotation -> Range Source #
HasRange ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: ArgInfo -> Range Source #
HasRange Cohesion Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Cohesion -> Range Source #
HasRange Erased Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Erased -> Range Source #
HasRange Fixity Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Fixity -> Range Source #
HasRange Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Hiding -> Range Source #
HasRange IsInstance Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: IsInstance -> Range Source #
HasRange IsMacro Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: IsMacro -> Range Source #
HasRange Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Modality -> Range Source #
HasRange NotationPart Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: NotationPart -> Range Source #
HasRange Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Origin -> Range Source #
HasRange OriginIrrelevant Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: OriginIrrelevant -> Range Source #
HasRange OriginRelevant Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: OriginRelevant -> Range Source #
HasRange OriginShapeIrrelevant Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: OriginShapeIrrelevant -> Range Source #
HasRange PatternOrCopattern Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: PatternOrCopattern -> Range Source #
HasRange PolarityModality Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: PolarityModality -> Range Source #
HasRange Q0Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Q0Origin -> Range Source #
HasRange Q1Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Q1Origin -> Range Source #
HasRange Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Quantity -> Range Source #
HasRange QωOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: QωOrigin -> Range Source #
HasRange Relevance Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Relevance -> Range Source #
HasRange Induction Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Induction -> Range Source #
HasRange KwRange Source # |
Instance details Defined in Agda.Syntax.Common.KeywordRange Methods getRange :: KwRange -> Range Source #
HasRange AsName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: AsName -> Range Source #
HasRange Binder Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Binder -> Range Source #
HasRange BoundName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: BoundName -> Range Source #
HasRange Declaration Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Declaration -> Range Source #
HasRange DoStmt Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: DoStmt -> Range Source #
HasRange Expr Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Expr -> Range Source #
HasRange LHS Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LHS -> Range Source #
HasRange LHSCore Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LHSCore -> Range Source #
HasRange LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range Source #
HasRange LamClause Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamClause -> Range Source #
HasRange ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: ModuleApplication -> Range Source #
HasRange ModuleAssignment Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: ModuleAssignment -> Range Source #
HasRange Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Pattern -> Range Source #
HasRange Pragma Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Pragma -> Range Source #
HasRange RHS Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: RHS -> Range Source #
HasRange RecordDirective Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: RecordDirective -> Range Source #
HasRange TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: TypedBinding -> Range Source #
HasRange WhereClause Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: WhereClause -> Range Source #
HasRange Attr Source # |
Instance details Defined in Agda.Syntax.Concrete.Attribute Methods getRange :: Attr -> Range Source #
HasRange Attribute Source # |
Instance details Defined in Agda.Syntax.Concrete.Attribute Methods getRange :: Attribute -> Range Source #
HasRange DeclarationException Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationException -> Range Source #
HasRange DeclarationException' Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationException' -> Range Source #
HasRange DeclarationWarning Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationWarning -> Range Source #
HasRange DeclarationWarning' Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationWarning' -> Range Source #
HasRange NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods getRange :: NiceDeclaration -> Range Source #
HasRange Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: Name -> Range Source #
HasRange QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: QName -> Range Source #
HasRange AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: AppInfo -> Range Source #
HasRange ConPatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: ConPatInfo -> Range Source #
HasRange DeclInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: DeclInfo -> Range Source #
HasRange ExprInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: ExprInfo -> Range Source #
HasRange LHSInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: LHSInfo -> Range Source #
HasRange LetInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: LetInfo -> Range Source #
HasRange MetaInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: MetaInfo -> Range Source #
HasRange ModuleInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: ModuleInfo -> Range Source #
HasRange MutualInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: MutualInfo -> Range Source #
HasRange PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: PatInfo -> Range Source #
HasRange Clause Source # |
Instance details Defined in Agda.Syntax.Internal Methods getRange :: Clause -> Range Source #
HasRange ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods getRange :: ConHead -> Range Source #
HasRange ParseError Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseError -> Range Source #
HasRange ParseWarning Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseWarning -> Range Source #
HasRange Token Source # |
Instance details Defined in Agda.Syntax.Parser.Tokens Methods getRange :: Token -> Range Source #
HasRange Interval Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: Interval -> Range Source #
HasRange Range Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: Range -> Range Source #
HasRange AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods getRange :: AbstractName -> Range Source #
HasRange RawTopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods getRange :: RawTopLevelModuleName -> Range Source #
HasRange Call Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Call -> Range Source #
HasRange CallInfo Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: CallInfo -> Range Source #
HasRange CompilerPragma Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: CompilerPragma -> Range Source #
HasRange Constraint Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Constraint -> Range Source #
HasRange MetaInfo Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: MetaInfo -> Range Source #
HasRange MetaVariable Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: MetaVariable -> Range Source #
HasRange ProblemConstraint Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: ProblemConstraint -> Range Source #
HasRange TCErr Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: TCErr -> Range Source #
HasRange TCWarning Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: TCWarning -> Range Source #
HasRange Item Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods getRange :: Item -> Range Source #
HasRange () Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: () -> Range Source #
HasRange Bool Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: Bool -> Range Source #
HasRange a => HasRange (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Binder' a -> Range Source #
HasRange a => HasRange (Clause' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Clause' a -> Range Source #
HasRange (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LHSCore' e -> Range Source #
HasRange (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Pattern' e -> Range Source #
HasRange a => HasRange (Arg a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Arg a -> Range Source #
HasRange a => HasRange (HasEta' a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: HasEta' a -> Range Source #
HasRange a => HasRange (MaybePlaceholder a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: MaybePlaceholder a -> Range Source #
HasRange (Ranged a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Ranged a -> Range Source #
HasRange a => HasRange (RecordDirectives' a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: RecordDirectives' a -> Range Source #
HasRange a => HasRange (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: WithHiding a -> Range Source #
HasRange a => HasRange (WithOrigin a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: WithOrigin a -> Range Source #
HasRange a => HasRange (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: FieldAssignment' a -> Range Source #
HasRange e => HasRange (OpApp e) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: OpApp e -> Range Source #
HasRange (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: TacticAttribute' a -> 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 a => HasRange (PrintRange a) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: PrintRange a -> Range Source #
HasRange (TopLevelModuleName' Range) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: TopLevelModuleName' Range -> 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 (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 (Set1 a) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: Set1 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 [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 b) => HasRange (ImportDirective' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: ImportDirective' a b -> Range Source #
(HasRange a, HasRange b) => HasRange (ImportedName' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: ImportedName' a b -> Range Source #
HasRange a => HasRange (Named name a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Named name a -> 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 (Using' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Using' a b -> 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 (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 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 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 (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 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 HasRangeWithoutFile a where Source #

Things that have a `RangeWithoutFile` are instances of this class.

Minimal complete definition

Nothing

Methods

getRangeWithoutFile :: a -> RangeWithoutFile Source #

default getRangeWithoutFile :: forall (t :: Type -> Type) b. (Foldable t, HasRangeWithoutFile b, t b ~ a) => a -> RangeWithoutFile Source #

#### Instances

Instances details

HasRangeWithoutFile Layer Source # |
Instance details Defined in Agda.Syntax.Parser.Literate Methods getRangeWithoutFile :: Layer -> RangeWithoutFile Source #
HasRangeWithoutFile Token Source # |
Instance details Defined in Agda.Syntax.Parser.Tokens Methods getRangeWithoutFile :: Token -> RangeWithoutFile Source #
HasRangeWithoutFile IntervalWithoutFile Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: IntervalWithoutFile -> RangeWithoutFile Source #
HasRangeWithoutFile RangeWithoutFile Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: RangeWithoutFile -> RangeWithoutFile Source #
HasRangeWithoutFile () Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: () -> RangeWithoutFile Source #
HasRangeWithoutFile Bool Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: Bool -> RangeWithoutFile Source #
HasRangeWithoutFile a => HasRangeWithoutFile (List1 a) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: List1 a -> RangeWithoutFile Source #
HasRangeWithoutFile a => HasRangeWithoutFile (List2 a) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: List2 a -> RangeWithoutFile Source #
HasRangeWithoutFile a => HasRangeWithoutFile (Set1 a) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: Set1 a -> RangeWithoutFile Source #
HasRangeWithoutFile a => HasRangeWithoutFile (Maybe a) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: Maybe a -> RangeWithoutFile Source #
HasRangeWithoutFile a => HasRangeWithoutFile [a] Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: [a] -> RangeWithoutFile Source #
(HasRangeWithoutFile a, HasRangeWithoutFile b) => HasRangeWithoutFile (Either a b) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: Either a b -> RangeWithoutFile Source #
(HasRangeWithoutFile a, HasRangeWithoutFile b) => HasRangeWithoutFile (a, b) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: (a, b) -> RangeWithoutFile Source #
(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c) => HasRangeWithoutFile (a, b, c) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: (a, b, c) -> RangeWithoutFile Source #
(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d) => HasRangeWithoutFile (a, b, c, d) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: (a, b, c, d) -> RangeWithoutFile Source #
(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d, HasRangeWithoutFile e) => HasRangeWithoutFile (a, b, c, d, e) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: (a, b, c, d, e) -> RangeWithoutFile Source #
(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d, HasRangeWithoutFile e, HasRangeWithoutFile f) => HasRangeWithoutFile (a, b, c, d, e, f) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: (a, b, c, d, e, f) -> RangeWithoutFile Source #
(HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d, HasRangeWithoutFile e, HasRangeWithoutFile f, HasRangeWithoutFile g) => HasRangeWithoutFile (a, b, c, d, e, f, g) Source # |
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: (a, b, c, d, e, f, g) -> RangeWithoutFile 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 :: forall (f :: Type -> Type) b. (Functor f, SetRange b, f b ~ a) => Range -> a -> a Source #

#### Instances

Instances details

SetRange BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods setRange :: Range -> BindName -> BindName Source #
SetRange ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> ModuleName -> ModuleName Source #
SetRange Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> Name -> Name Source #
SetRange QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> QName -> QName Source #
SetRange Cohesion Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Cohesion -> Cohesion Source #
SetRange NotationPart Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> NotationPart -> NotationPart Source #
SetRange OriginIrrelevant Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> OriginIrrelevant -> OriginIrrelevant Source #
SetRange OriginRelevant Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> OriginRelevant -> OriginRelevant Source #
SetRange OriginShapeIrrelevant Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> OriginShapeIrrelevant -> OriginShapeIrrelevant Source #
SetRange PolarityModality Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> PolarityModality -> PolarityModality Source #
SetRange Q0Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Q0Origin -> Q0Origin Source #
SetRange Q1Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Q1Origin -> Q1Origin Source #
SetRange Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Quantity -> Quantity Source #
SetRange QωOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> QωOrigin -> QωOrigin Source #
SetRange Relevance Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Relevance -> Relevance Source #
SetRange Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete Methods setRange :: Range -> Pattern -> Pattern Source #
SetRange TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods setRange :: Range -> TypedBinding -> TypedBinding Source #
SetRange Attr Source # |
Instance details Defined in Agda.Syntax.Concrete.Attribute Methods setRange :: Range -> Attr -> Attr Source #
SetRange Attribute Source # |
Instance details Defined in Agda.Syntax.Concrete.Attribute Methods setRange :: Range -> Attribute -> Attribute Source #
SetRange Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> Name -> Name Source #
SetRange QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> QName -> QName Source #
SetRange ConPatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> ConPatInfo -> ConPatInfo Source #
SetRange DeclInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> DeclInfo -> DeclInfo Source #
SetRange ModuleInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> ModuleInfo -> ModuleInfo Source #
SetRange PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> PatInfo -> PatInfo Source #
SetRange ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods setRange :: Range -> ConHead -> ConHead Source #
SetRange Range Source # |
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> Range -> Range Source #
SetRange AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods setRange :: Range -> AbstractName -> AbstractName Source #
SetRange RawTopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods setRange :: Range -> RawTopLevelModuleName -> RawTopLevelModuleName Source #
SetRange MetaInfo Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods setRange :: Range -> MetaInfo -> MetaInfo Source #
SetRange MetaVariable Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods setRange :: Range -> MetaVariable -> MetaVariable Source #
SetRange (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods setRange :: Range -> Pattern' a -> Pattern' a Source #
SetRange a => SetRange (Arg a) Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Arg a -> Arg a Source #
SetRange a => SetRange (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> WithHiding a -> WithHiding a Source #
SetRange a => SetRange (WithOrigin a) Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> WithOrigin a -> WithOrigin a Source #
SetRange (DefInfo' t) Source # |
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> DefInfo' t -> DefInfo' t Source #
SetRange a => SetRange (PrintRange a) Source # |
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> PrintRange a -> PrintRange a Source #
SetRange (TopLevelModuleName' Range) Source # |
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> TopLevelModuleName' Range -> TopLevelModuleName' Range 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 [a] Source # |
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> [a] -> [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 :: forall (f :: Type -> Type) b. (Functor f, KillRange b, f b ~ a) => KillRangeT a Source #

#### Instances

Instances details

KillRange BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT BindName Source #
KillRange DataDefParams Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT DataDefParams Source #
KillRange Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Declaration Source #
KillRange Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Expr Source #
KillRange GeneralizeTelescope Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT GeneralizeTelescope Source #
KillRange LHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LHS Source #
KillRange LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LamBinding Source #
KillRange LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LetBinding Source #
KillRange ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ModuleApplication Source #
KillRange ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ProblemEq Source #
KillRange RHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT RHS Source #
KillRange RecordConName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT RecordConName Source #
KillRange ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ScopeCopyInfo Source #
KillRange SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT SpineLHS Source #
KillRange TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT TypedBinding Source #
KillRange TypedBindingInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT TypedBindingInfo Source #
KillRange WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT WhereDeclarations Source #
KillRange AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT AmbiguousQName Source #
KillRange ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT ModuleName Source #
KillRange Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT Name Source #
KillRange QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT QName Source #
KillRange Suffix Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Suffix Source #
KillRange BuiltinId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods killRange :: KillRangeT BuiltinId Source #
KillRange PrimitiveId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods killRange :: KillRangeT PrimitiveId Source #
KillRange Access Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Access Source #
KillRange Annotation Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Annotation Source #
KillRange ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT ArgInfo Source #
KillRange BinderNameOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT BinderNameOrigin Source #
KillRange Catchall Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Catchall Source #
KillRange Cohesion Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Cohesion Source #
KillRange ConOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT ConOrigin Source #
KillRange CoverageCheck Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT CoverageCheck Source #
KillRange Erased Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Erased Source #
KillRange ExpandedEllipsis Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT ExpandedEllipsis Source #
KillRange Fixity Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Fixity Source #
KillRange Fixity' Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Fixity' Source #
KillRange FreeVariables Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT FreeVariables Source #
KillRange Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Hiding Source #
KillRange InteractionId Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT InteractionId Source #
KillRange IsAbstract Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsAbstract Source #
KillRange IsInstance Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsInstance Source #
KillRange IsMacro Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsMacro Source #
KillRange IsOpaque Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsOpaque Source #
KillRange Language Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Language Source #
KillRange Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Modality Source #
KillRange NameId Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT NameId Source #
KillRange NotationPart Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT NotationPart Source #
KillRange OpaqueId Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT OpaqueId Source #
KillRange Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Origin Source #
KillRange OriginIrrelevant Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT OriginIrrelevant Source #
KillRange OriginRelevant Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT OriginRelevant Source #
KillRange OriginShapeIrrelevant Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT OriginShapeIrrelevant Source #
KillRange OverlapMode Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT OverlapMode Source #
KillRange PatternOrCopattern Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT PatternOrCopattern Source #
KillRange PolarityModality Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT PolarityModality Source #
KillRange PositivityCheck Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT PositivityCheck Source #
KillRange ProjOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT ProjOrigin Source #
KillRange Q0Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Q0Origin Source #
KillRange Q1Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Q1Origin Source #
KillRange Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Quantity Source #
KillRange QωOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT QωOrigin Source #
KillRange Relevance Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Relevance Source #
KillRange UniverseCheck Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT UniverseCheck Source #
KillRange Induction Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Induction Source #
KillRange KwRange Source # |
Instance details Defined in Agda.Syntax.Common.KeywordRange Methods killRange :: KillRangeT KwRange Source #
KillRange AsName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT AsName Source #
KillRange Binder Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Binder Source #
KillRange BoundName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT BoundName Source #
KillRange Declaration Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Declaration Source #
KillRange DoStmt Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT DoStmt Source #
KillRange Expr Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Expr Source #
KillRange LHS Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LHS Source #
KillRange LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamBinding Source #
KillRange LamClause Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamClause Source #
KillRange ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT ModuleApplication Source #
KillRange ModuleAssignment Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT ModuleAssignment Source #
KillRange Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Pattern Source #
KillRange Pragma Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Pragma Source #
KillRange RHS Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT RHS Source #
KillRange RecordDirective Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT RecordDirective Source #
KillRange TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT TypedBinding Source #
KillRange WhereClause Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT WhereClause Source #
KillRange Attr Source # |
Instance details Defined in Agda.Syntax.Concrete.Attribute Methods killRange :: KillRangeT Attr Source #
KillRange Attribute Source # |
Instance details Defined in Agda.Syntax.Concrete.Attribute Methods killRange :: KillRangeT Attribute Source #
KillRange Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT Name Source #
KillRange QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT QName Source #
KillRange AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT AppInfo Source #
KillRange ConPatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ConPatInfo Source #
KillRange DeclInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT DeclInfo Source #
KillRange ExprInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ExprInfo Source #
KillRange LHSInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT LHSInfo Source #
KillRange LetInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT LetInfo Source #
KillRange MetaInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT MetaInfo Source #
KillRange ModuleInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ModuleInfo Source #
KillRange MutualInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT MutualInfo Source #
KillRange PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT PatInfo Source #
KillRange Clause Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Clause Source #
KillRange ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT ConHead Source #
KillRange ConPatternInfo Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT ConPatternInfo Source #
KillRange DBPatVar Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT DBPatVar Source #
KillRange DataOrRecord Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT DataOrRecord Source #
KillRange Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Level Source #
KillRange PatOrigin Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT PatOrigin Source #
KillRange PatternInfo Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT PatternInfo Source #
KillRange PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT PlusLevel Source #
KillRange Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Sort Source #
KillRange Substitution Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Substitution Source #
KillRange Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Term Source #
KillRange Literal Source # |
Instance details Defined in Agda.Syntax.Literal Methods killRange :: KillRangeT Literal Source #
KillRange Range Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Range Source #
KillRange ScopeInfo Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods killRange :: KillRangeT ScopeInfo Source #
KillRange RawTopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods killRange :: KillRangeT RawTopLevelModuleName Source #
KillRange Compiled Source # |
Instance details Defined in Agda.Syntax.Treeless Methods killRange :: KillRangeT Compiled Source #
KillRange CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT CompiledClauses Source #
KillRange SplitTag Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods killRange :: KillRangeT SplitTag Source #
KillRange BuiltinSort Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT BuiltinSort Source #
KillRange CompKit Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT CompKit Source #
KillRange CompiledRepresentation Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT CompiledRepresentation Source #
KillRange Definition Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Definition Source #
KillRange Definitions Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Definitions Source #
KillRange Defn Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Defn Source #
KillRange DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT DisplayForm Source #
KillRange DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT DisplayTerm Source #
KillRange DoGeneralize Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT DoGeneralize Source #
KillRange EtaEquality Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT EtaEquality Source #
KillRange ExtLamInfo Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT ExtLamInfo Source #
KillRange FunctionFlag Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT FunctionFlag Source #
KillRange InstanceInfo Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT InstanceInfo Source #
KillRange InstanceTable Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT InstanceTable Source #
KillRange IsForced Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT IsForced Source #
KillRange MutualId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT MutualId Source #
KillRange NLPSort Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT NLPSort Source #
KillRange NLPType Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT NLPType Source #
KillRange NLPat Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT NLPat Source #
KillRange NumGeneralizableArgs Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT NumGeneralizableArgs Source #
KillRange ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT ProjLams Source #
KillRange Projection Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Projection Source #
KillRange ProjectionLikenessMissing Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT ProjectionLikenessMissing Source #
KillRange RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT RewriteRule Source #
KillRange RewriteRuleMap Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT RewriteRuleMap Source #
KillRange Section Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Section Source #
KillRange Sections Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Sections Source #
KillRange Signature Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Signature Source #
KillRange System Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT System Source #
KillRange TermHead Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT TermHead Source #
KillRange Polarity Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Polarity Source #
KillRange Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods killRange :: KillRangeT Occurrence Source #
KillRange Permutation Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Permutation Source #
KillRange Void Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Void Source #
KillRange Integer Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Integer Source #
KillRange String Source # | Overlaps with `KillRange [a]`.
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT String Source #
KillRange () Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT () Source #
KillRange Bool Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Bool Source #
KillRange Int Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Int Source #
KillRange a => KillRange (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Binder' a) Source #
KillRange a => KillRange (Clause' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Clause' a) Source #
KillRange e => KillRange (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (LHSCore' e) Source #
KillRange e => KillRange (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Pattern' e) Source #
KillRange a => KillRange (Arg a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Arg a) Source #
KillRange a => KillRange (HasEta' a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (HasEta' a) Source #
KillRange a => KillRange (MaybePlaceholder a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (MaybePlaceholder a) Source #
KillRange (Ranged a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Ranged a) Source #
KillRange a => KillRange (RecordDirectives' a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (RecordDirectives' a) Source #
KillRange m => KillRange (TerminationCheck m) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (TerminationCheck m) Source #
KillRange a => KillRange (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (WithHiding a) Source #
KillRange a => KillRange (WithOrigin a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (WithOrigin a) Source #
KillRange a => KillRange (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (FieldAssignment' a) Source #
KillRange e => KillRange (OpApp e) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (OpApp e) Source #
KillRange (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (TacticAttribute' a) Source #
KillRange x => KillRange (ThingWithFixity x) Source # |
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) Source #
KillRange t => KillRange (DefInfo' t) Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT (DefInfo' t) Source #
KillRange a => KillRange (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Abs a) Source #
KillRange a => KillRange (Blocked a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Blocked a) Source #
KillRange a => KillRange (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Pattern' a) Source #
KillRange a => KillRange (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Tele a) Source #
KillRange a => KillRange (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Type' a) Source #
KillRange a => KillRange (Elim' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Elim Methods killRange :: KillRangeT (Elim' a) Source #
KillRange a => KillRange (PrintRange a) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (PrintRange a) Source #
KillRange (TopLevelModuleName' Range) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (TopLevelModuleName' Range) Source #
KillRange c => KillRange (Case c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (Case c) Source #
KillRange c => KillRange (WithArity c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (WithArity c) Source #
KillRange a => KillRange (SplitTree' a) Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods killRange :: KillRangeT (SplitTree' a) Source #
(KillRange a, Ord a) => KillRange (DiscrimTree a) Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree.Types Methods killRange :: KillRangeT (DiscrimTree a) Source #
KillRange a => KillRange (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (Closure a) Source #
KillRange c => KillRange (FunctionInverse' c) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (FunctionInverse' c) Source #
KillRange a => KillRange (Open a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (Open a) Source #
KillRange a => KillRange (List1 a) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (List1 a) Source #
KillRange a => KillRange (List2 a) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (List2 a) Source #
KillRange a => KillRange (Drop a) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Drop a) Source #
(Ord a, KillRange a) => KillRange (Set1 a) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Set1 a) Source #
KillRange (SmallSet FunctionFlag) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (SmallSet FunctionFlag) Source #
(Ord a, KillRange a) => KillRange (Set a) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Set a) Source #
KillRange a => KillRange (Maybe a) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Maybe a) Source #
KillRange a => KillRange (Maybe a) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Maybe a) Source #
KillRange a => KillRange [a] Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT [a] Source #
(KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportDirective' a b) Source #
(KillRange a, KillRange b) => KillRange (ImportedName' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportedName' a b) Source #
(KillRange name, KillRange a) => KillRange (Named name a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Named name a) Source #
(KillRange a, KillRange b) => KillRange (Renaming' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Renaming' a b) Source #
(KillRange a, KillRange b) => KillRange (Using' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Using' a b) 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 (Map k a) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Map k a) Source #
(KillRange a, KillRange b) => KillRange (Either a b) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Either a b) Source #
(KillRange a, KillRange b) => KillRange (a, b) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (a, b) 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 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 #
(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 #

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.

class KILLRANGE t (b :: Bool) where Source #

Methods

killRangeN :: t -> t Source #

#### Instances

Instances details

IsBase t ~ 'True => KILLRANGE t 'True Source # |
Instance details Defined in Agda.Syntax.Position Methods killRangeN :: t -> t Source #
KILLRANGE t (IsBase t) => KILLRANGE (a -> t) 'False Source # |
Instance details Defined in Agda.Syntax.Position Methods killRangeN :: (a -> t) -> a -> t Source #

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

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

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

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 :: BeginningOfFile a => a -> Range Source #

Return an empty range (a single, empty interval) at the beginning of the file.

interleaveRanges :: HasRangeWithoutFile 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.