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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Syntax.Position

Contents

- Positions
- Intervals
- Ranges
- Orphan instances

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 :: !Int32
  - posLine :: !Int32
  - posCol :: !Int32
  }
- type SrcFile = Maybe AbsolutePath
- positionInvariant :: Position' a -> Bool
- startPos :: Maybe AbsolutePath -> Position
- movePos :: Position' a -> Char -> Position' a
- movePosByString :: Position' a -> String -> Position' a
- backupPos :: Position' a -> Position' a
- startPos' :: a -> Position' a
- type Interval = Interval' SrcFile
- type IntervalWithoutFile = Interval' ()
- data Interval' a = Interval {
  - iStart, iEnd :: !(Position' a)
  }
- intervalInvariant :: Ord a => Interval' a -> Bool
- posToInterval :: a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
- getIntervalFile :: Interval' a -> a
- iLength :: Interval' a -> Int32
- fuseIntervals :: Ord a => Interval' a -> Interval' a -> Interval' a
- setIntervalFile :: a -> Interval' b -> Interval' a
- type Range = Range' SrcFile
- 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
- rangeIntervals :: Range' a -> [IntervalWithoutFile]
- rangeFile :: Range -> SrcFile
- 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 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)
- killRange1 :: KillRange a => (a -> b) -> a -> b
- killRange2 :: (KillRange a, KillRange b) => (a -> b -> c) -> a -> b -> c
- killRange3 :: (KillRange a, KillRange b, KillRange c) => (a -> b -> c -> d) -> a -> b -> c -> d
- killRange4 :: (KillRange a, KillRange b, KillRange c, KillRange d) => (a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
- killRange5 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e) => (a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
- killRange6 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f) => (a -> b -> c -> d -> e -> f -> g) -> a -> b -> c -> d -> e -> f -> g
- killRange7 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g) => (a -> b -> c -> d -> e -> f -> g -> h) -> a -> b -> c -> d -> e -> f -> g -> h
- killRange8 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h) => (a -> b -> c -> d -> e -> f -> g -> h -> i) -> a -> b -> c -> d -> e -> f -> g -> h -> i
- killRange9 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j
- killRange10 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k
- killRange11 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l
- killRange12 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m
- killRange13 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n
- killRange14 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o
- killRange15 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p
- killRange16 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q
- killRange17 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r
- killRange18 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q, KillRange r) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s
- killRange19 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q, KillRange r, KillRange s) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> t) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> t
- withRangeOf :: (SetRange t, HasRange u) => t -> u -> t
- fuseRange :: (HasRange u, HasRange t) => u -> t -> Range
- fuseRanges :: Ord a => Range' a -> Range' a -> Range' a
- beginningOf :: Range -> Range
- beginningOfFile :: Range -> Range
- interleaveRanges :: HasRange 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 :: !Int32

  Position, counting from 1.

- posLine :: !Int32

  Line number, counting from 1.

- posCol :: !Int32

  Column number, counting from 1.

#### Instances

Instances details

Pretty PositionWithoutFile Source # |
Instance details Defined in Agda.Syntax.Position Methods pretty :: PositionWithoutFile -> Doc Source # prettyPrec :: Int -> PositionWithoutFile -> Doc Source # prettyList :: [PositionWithoutFile] -> Doc 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 #
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 #
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 #
EncodeTCM (Position' ()) Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Position' () -> TCM Value Source #
EmbPrj a => EmbPrj (Position' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Position' a -> S Int32 Source # icod_ :: Position' a -> S Int32 Source # value :: Int32 -> R (Position' a) Source #
Pretty a => Pretty (Position' (Maybe a)) Source # |
Instance details Defined in Agda.Syntax.Position Methods pretty :: Position' (Maybe a) -> Doc Source # prettyPrec :: Int -> Position' (Maybe a) -> Doc Source # prettyList :: [Position' (Maybe a)] -> Doc Source #
ToJSON (Position' ()) Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: Position' () -> Value # toEncoding :: Position' () -> Encoding # toJSONList :: [Position' ()] -> Value # toEncodingList :: [Position' ()] -> Encoding #
Data a => Data (Position' a) Source # |

Instance details

Defined in Agda.Syntax.Position

Methods

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

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

toConstr :: Position' a -> Constr Source #

dataTypeOf :: Position' a -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Generic (Position' a) Source # |
Instance details Defined in Agda.Syntax.Position Associated Types type Rep (Position' a) :: Type -> Type Source # 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.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "Pn" 'PrefixI 'True) ((S1 ('MetaSel ('Just "srcFile") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a) :*: S1 ('MetaSel ('Just "posPos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int32)) :*: (S1 ('MetaSel ('Just "posLine") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int32) :*: S1 ('MetaSel ('Just "posCol") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int32))))

type SrcFile = Maybe AbsolutePath Source #

positionInvariant :: Position' a -> Bool Source #

startPos :: Maybe AbsolutePath -> Position Source #

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

movePos :: Position' a -> Char -> Position' a Source #

Advance the position by one character. A newline character (`'n'`) moves the position to the first character in the next line. Any other character moves the position to the next column.

movePosByString :: Position' a -> String -> Position' a Source #

Advance the position by a string.

    movePosByString = foldl' movePos

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

Backup the position by one character.

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

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

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

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

Fields

- iStart, iEnd :: !(Position' a)

#### Instances

Instances details

HasRange Interval Source # |
Instance details Defined in Agda.Syntax.Position Methods getRange :: Interval -> Range Source #
Pretty IntervalWithoutFile Source # |
Instance details Defined in Agda.Syntax.Position Methods pretty :: IntervalWithoutFile -> Doc Source # prettyPrec :: Int -> IntervalWithoutFile -> Doc Source # prettyList :: [IntervalWithoutFile] -> Doc 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 #
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 #
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 #
EmbPrj a => EmbPrj (Interval' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Interval' a -> S Int32 Source # icod_ :: Interval' a -> S Int32 Source # value :: Int32 -> R (Interval' a) Source #
Pretty a => Pretty (Interval' (Maybe a)) Source # |
Instance details Defined in Agda.Syntax.Position Methods pretty :: Interval' (Maybe a) -> Doc Source # prettyPrec :: Int -> Interval' (Maybe a) -> Doc Source # prettyList :: [Interval' (Maybe a)] -> Doc Source #
Data a => Data (Interval' a) Source # |

Instance details

Defined in Agda.Syntax.Position

Methods

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

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

toConstr :: Interval' a -> Constr Source #

dataTypeOf :: Interval' a -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Generic (Interval' a) Source # |
Instance details Defined in Agda.Syntax.Position Associated Types type Rep (Interval' a) :: Type -> Type Source # 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.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "Interval" 'PrefixI 'True) (S1 ('MetaSel ('Just "iStart") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Position' a)) :*: S1 ('MetaSel ('Just "iEnd") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Position' a))))

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

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

Converts a file name and two positions to an interval.

getIntervalFile :: Interval' a -> a Source #

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

iLength :: Interval' a -> Int32 Source #

The length of an interval.

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

Finds the least interval which covers the arguments.

Precondition: The intervals must point to the same file.

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

Sets the `srcFile` components of the interval.

# Ranges

type Range = Range' SrcFile 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 #
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 #
EmbPrj Range Source # | Ranges are always deserialised as `noRange`.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Range -> S Int32 Source # icod_ :: Range -> S Int32 Source # value :: Int32 -> R Range Source #
Subst Range Source # |
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg Range Source # Methods applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source #
ToJSON Range Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: Range -> Value # toEncoding :: Range -> Encoding # toJSONList :: [Range] -> Value # toEncodingList :: [Range] -> Encoding #
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 #
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 #
LensClosure Range MetaInfo Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lensClosure :: Lens' (Closure Range) MetaInfo Source #
LensClosure Range MetaVariable Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lensClosure :: Lens' (Closure Range) MetaVariable Source #
Null (Range' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods empty :: Range' a Source # null :: Range' a -> Bool Source #
Pretty a => Pretty (Range' (Maybe a)) Source # |
Instance details Defined in Agda.Syntax.Position Methods pretty :: Range' (Maybe a) -> Doc Source # prettyPrec :: Int -> Range' (Maybe a) -> Doc Source # prettyList :: [Range' (Maybe a)] -> Doc Source #
Data a => Data (Range' a) Source # |

Instance details

Defined in Agda.Syntax.Position

Methods

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

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

toConstr :: Range' a -> Constr Source #

dataTypeOf :: Range' a -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Semigroup 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 #
Semigroup 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) :: Type -> Type Source # 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 #
NFData a => NFData (Range' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods rnf :: Range' a -> () 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.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "NoRange" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Range" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Seq IntervalWithoutFile))))

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

Range invariant.

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

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

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

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

Precondition: `consecutiveAndSeparated`.

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

Converts a file name and an interval to a range.

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

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

rangeFile :: Range -> SrcFile Source #

The file the range is pointing to.

rightMargin :: Range -> Range Source #

Conflate a range to its right margin.

noRange :: Range' a Source #

Ranges between two unknown positions

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

Converts two positions to a range.

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

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

Converts a file name and two positions to a range.

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

The initial position in the range, if any.

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

The initial position in the range, if any.

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

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

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

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

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

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

rangeToIntervalWithFile :: Range' a -> Maybe (Interval' a) Source #

Converts a range to an interval, if possible.

continuous :: Range' a -> Range' a Source #

Returns the shortest continuous range containing the given one.

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

Removes gaps between intervals on the same line.

newtype PrintRange a Source #

Wrapper to indicate that range should be printed.

Constructors

PrintRange a |

#### Instances

Instances details

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 #
(Pretty a, HasRange a) => Pretty (PrintRange a) Source # |
Instance details Defined in Agda.Syntax.Position Methods pretty :: PrintRange a -> Doc Source # prettyPrec :: Int -> PrintRange a -> Doc Source # prettyList :: [PrintRange a] -> Doc 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 :: (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 GenPart Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: GenPart -> Range Source #
HasRange Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Hiding -> Range Source #
HasRange Induction Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Induction -> 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 Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Origin -> Range Source #
HasRange PatternOrCopattern Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: PatternOrCopattern -> 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 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 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 TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: TopLevelModuleName -> 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 Layer Source # |
Instance details Defined in Agda.Syntax.Parser.Literate Methods getRange :: Layer -> 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 Call Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Call -> Range Source #
HasRange CompilerPragma Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base 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 #
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 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 (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 HasRange a => SetRange a where Source #

If it is also possible to set the range, this is the class.

Instances should satisfy ``getRange` (`setRange` r x) == r`.

Minimal complete definition

Nothing

Methods

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

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

#### Instances

Instances details

SetRange 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 GenPart Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> GenPart -> GenPart 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 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 TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> TopLevelModuleName -> TopLevelModuleName 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 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 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 :: (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 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 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 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 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 Delayed Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Delayed 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 GenPart Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT GenPart Source #
KillRange Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Hiding Source #
KillRange Induction Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Induction 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 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 Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Origin Source #
KillRange PatternOrCopattern Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT PatternOrCopattern 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 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 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 TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT TopLevelModuleName 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 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 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 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 Polarity Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Polarity 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 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 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 String Source # | Overlaps with `KillRange [a]`.
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT String Source #
KillRange Integer Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Integer 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 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 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 => 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 (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 b) => KillRange (Either a b) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Either a b) Source #
KillRange a => KillRange (Map k a) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Map k a) Source #
(KillRange a, KillRange b) => KillRange (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.

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

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

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

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

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

killRange6 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f) => (a -> b -> c -> d -> e -> f -> g) -> a -> b -> c -> d -> e -> f -> g Source #

killRange7 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g) => (a -> b -> c -> d -> e -> f -> g -> h) -> a -> b -> c -> d -> e -> f -> g -> h Source #

killRange8 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h) => (a -> b -> c -> d -> e -> f -> g -> h -> i) -> a -> b -> c -> d -> e -> f -> g -> h -> i Source #

killRange9 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j Source #

killRange10 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k Source #

killRange11 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l Source #

killRange12 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m Source #

killRange13 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n Source #

killRange14 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o Source #

killRange15 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p Source #

killRange16 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q Source #

killRange17 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r Source #

killRange18 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q, KillRange r) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s Source #

killRange19 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q, KillRange r, KillRange s) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> t) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> t Source #

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

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

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

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

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

`fuseRanges r r'` unions the ranges `r` and `r'`.

Meaning it finds the least range `r0` that covers `r` and `r'`.

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

beginningOf :: Range -> Range Source #

`beginningOf r` is an empty range (a single, empty interval) positioned at the beginning of `r`. If `r` does not have a beginning, then `noRange` is returned.

beginningOfFile :: Range -> Range Source #

`beginningOfFile r` is an empty range (a single, empty interval) at the beginning of `r`'s starting position's file. If there is no such position, then an empty range is returned.

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

Interleaves two streams of ranged elements

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

# Orphan instances

Semigroup AbsolutePath Source # | To get ``Semigroup` `Range``, we need a semigroup instance for `AbsolutePath`.
Instance details Methods (<>) :: AbsolutePath -> AbsolutePath -> AbsolutePath Source # sconcat :: NonEmpty AbsolutePath -> AbsolutePath Source # stimes :: Integral b => b -> AbsolutePath -> AbsolutePath Source #