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 :: !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
takeI :: String -> Interval' a -> Interval' a
dropI :: String -> Interval' a -> 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 t where
class HasRange t => SetRange t where
class KillRange a where
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 #

type PositionWithoutFile = Position' () #

data Position' a #

Represents a point in the input.

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

Note the invariant which positions have to satisfy: positionInvariant.

Constructors

Pn
Fields srcFile :: !a File. posPos :: !Int32 Position, counting from 1. posLine :: !Int32 Line number, counting from 1. posCol :: !Int32 Column number, counting from 1.

Instances

Functor Position' #
Instance details Defined in Agda.Syntax.Position Methods fmap :: (a -> b) -> Position' a -> Position' b # (<$) :: a -> Position' b -> Position' a #
Show PositionWithoutFile #
Instance details Defined in Agda.Syntax.Position Methods showsPrec :: Int -> PositionWithoutFile -> ShowS # show :: PositionWithoutFile -> String # showList :: [PositionWithoutFile] -> ShowS #
Foldable Position' #
Instance details Defined in Agda.Syntax.Position Methods fold :: Monoid m => Position' m -> m # foldMap :: Monoid m => (a -> m) -> Position' a -> m # foldr :: (a -> b -> b) -> b -> Position' a -> b # foldr' :: (a -> b -> b) -> b -> Position' a -> b # foldl :: (b -> a -> b) -> b -> Position' a -> b # foldl' :: (b -> a -> b) -> b -> Position' a -> b # foldr1 :: (a -> a -> a) -> Position' a -> a # foldl1 :: (a -> a -> a) -> Position' a -> a # toList :: Position' a -> [a] # null :: Position' a -> Bool # length :: Position' a -> Int # elem :: Eq a => a -> Position' a -> Bool # maximum :: Ord a => Position' a -> a # minimum :: Ord a => Position' a -> a # sum :: Num a => Position' a -> a # product :: Num a => Position' a -> a #
Traversable Position' #
Instance details Defined in Agda.Syntax.Position Methods traverse :: Applicative f => (a -> f b) -> Position' a -> f (Position' b) # sequenceA :: Applicative f => Position' (f a) -> f (Position' a) # mapM :: Monad m => (a -> m b) -> Position' a -> m (Position' b) # sequence :: Monad m => Position' (m a) -> m (Position' a) #
Pretty PositionWithoutFile #
Instance details Defined in Agda.Syntax.Position Methods pretty :: PositionWithoutFile -> Doc # prettyPrec :: Int -> PositionWithoutFile -> Doc # prettyList :: [PositionWithoutFile] -> Doc #
Eq a => Eq (Position' a) #
Instance details Defined in Agda.Syntax.Position Methods (==) :: Position' a -> Position' a -> Bool # (/=) :: Position' a -> Position' a -> Bool #
Data a => Data (Position' a) #
Instance details Defined in Agda.Syntax.Position Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Position' a -> c (Position' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Position' a) # toConstr :: Position' a -> Constr # dataTypeOf :: Position' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Position' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Position' a)) # gmapT :: (forall b. Data b => b -> b) -> Position' a -> Position' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Position' a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Position' a -> r # gmapQ :: (forall d. Data d => d -> u) -> Position' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Position' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Position' a -> m (Position' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Position' a -> m (Position' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Position' a -> m (Position' a) #
Ord a => Ord (Position' a) #
Instance details Defined in Agda.Syntax.Position Methods compare :: Position' a -> Position' a -> Ordering # (<) :: Position' a -> Position' a -> Bool # (<=) :: Position' a -> Position' a -> Bool # (>) :: Position' a -> Position' a -> Bool # (>=) :: Position' a -> Position' a -> Bool # max :: Position' a -> Position' a -> Position' a # min :: Position' a -> Position' a -> Position' a #
Read a => Read (Position' a) #
Instance details Defined in Agda.Interaction.InteractionTop Methods readsPrec :: Int -> ReadS (Position' a) # readList :: ReadS [Position' a] # readPrec :: ReadPrec (Position' a) # readListPrec :: ReadPrec [Position' a] #
Show a => Show (Position' (Maybe a)) #
Instance details Defined in Agda.Syntax.Position Methods showsPrec :: Int -> Position' (Maybe a) -> ShowS # show :: Position' (Maybe a) -> String # showList :: [Position' (Maybe a)] -> ShowS #
Generic (Position' a) #
Instance details Defined in Agda.Syntax.Position Associated Types type Rep (Position' a) :: * -> * # Methods from :: Position' a -> Rep (Position' a) x # to :: Rep (Position' a) x -> Position' a #
Pretty a => Pretty (Position' (Maybe a)) #
Instance details Defined in Agda.Syntax.Position Methods pretty :: Position' (Maybe a) -> Doc # prettyPrec :: Int -> Position' (Maybe a) -> Doc # prettyList :: [Position' (Maybe a)] -> Doc #
EmbPrj a => EmbPrj (Position' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Position' a -> S Int32 # icod_ :: Position' a -> S Int32 # value :: Int32 -> R (Position' a) #
type Rep (Position' a) #
Instance details Defined in Agda.Syntax.Position type Rep (Position' a) = D1 (MetaData "Position'" "Agda.Syntax.Position" "Agda-2.5.4-BdDHVHYPm5JDI57G7c5E26" 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 #

positionInvariant :: Position' a -> Bool #

startPos :: Maybe AbsolutePath -> Position #

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

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

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

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

Advance the position by a string.

movePosByString = foldl' movePos

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

Backup the position by one character.

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

startPos' :: a -> Position' a #

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

Intervals

type Interval = Interval' SrcFile #

type IntervalWithoutFile = Interval' () #

data Interval' a #

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

Note the invariant which intervals have to satisfy: intervalInvariant.

Constructors

Interval
Fields iStart, iEnd :: !(Position' a)

Instances

Functor Interval' #
Instance details Defined in Agda.Syntax.Position Methods fmap :: (a -> b) -> Interval' a -> Interval' b # (<$) :: a -> Interval' b -> Interval' a #
Show IntervalWithoutFile #
Instance details Defined in Agda.Syntax.Position Methods showsPrec :: Int -> IntervalWithoutFile -> ShowS # show :: IntervalWithoutFile -> String # showList :: [IntervalWithoutFile] -> ShowS #
Foldable Interval' #
Instance details Defined in Agda.Syntax.Position Methods fold :: Monoid m => Interval' m -> m # foldMap :: Monoid m => (a -> m) -> Interval' a -> m # foldr :: (a -> b -> b) -> b -> Interval' a -> b # foldr' :: (a -> b -> b) -> b -> Interval' a -> b # foldl :: (b -> a -> b) -> b -> Interval' a -> b # foldl' :: (b -> a -> b) -> b -> Interval' a -> b # foldr1 :: (a -> a -> a) -> Interval' a -> a # foldl1 :: (a -> a -> a) -> Interval' a -> a # toList :: Interval' a -> [a] # null :: Interval' a -> Bool # length :: Interval' a -> Int # elem :: Eq a => a -> Interval' a -> Bool # maximum :: Ord a => Interval' a -> a # minimum :: Ord a => Interval' a -> a # sum :: Num a => Interval' a -> a # product :: Num a => Interval' a -> a #
Traversable Interval' #
Instance details Defined in Agda.Syntax.Position Methods traverse :: Applicative f => (a -> f b) -> Interval' a -> f (Interval' b) # sequenceA :: Applicative f => Interval' (f a) -> f (Interval' a) # mapM :: Monad m => (a -> m b) -> Interval' a -> m (Interval' b) # sequence :: Monad m => Interval' (m a) -> m (Interval' a) #
Pretty IntervalWithoutFile #
Instance details Defined in Agda.Syntax.Position Methods pretty :: IntervalWithoutFile -> Doc # prettyPrec :: Int -> IntervalWithoutFile -> Doc # prettyList :: [IntervalWithoutFile] -> Doc #
HasRange Interval #
Instance details Defined in Agda.Syntax.Position Methods getRange :: Interval -> Range #
Eq a => Eq (Interval' a) #
Instance details Defined in Agda.Syntax.Position Methods (==) :: Interval' a -> Interval' a -> Bool # (/=) :: Interval' a -> Interval' a -> Bool #
Data a => Data (Interval' a) #
Instance details Defined in Agda.Syntax.Position Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Interval' a -> c (Interval' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Interval' a) # toConstr :: Interval' a -> Constr # dataTypeOf :: Interval' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Interval' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Interval' a)) # gmapT :: (forall b. Data b => b -> b) -> Interval' a -> Interval' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Interval' a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Interval' a -> r # gmapQ :: (forall d. Data d => d -> u) -> Interval' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Interval' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Interval' a -> m (Interval' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Interval' a -> m (Interval' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Interval' a -> m (Interval' a) #
Ord a => Ord (Interval' a) #
Instance details Defined in Agda.Syntax.Position Methods compare :: Interval' a -> Interval' a -> Ordering # (<) :: Interval' a -> Interval' a -> Bool # (<=) :: Interval' a -> Interval' a -> Bool # (>) :: Interval' a -> Interval' a -> Bool # (>=) :: Interval' a -> Interval' a -> Bool # max :: Interval' a -> Interval' a -> Interval' a # min :: Interval' a -> Interval' a -> Interval' a #
Read a => Read (Interval' a) #
Instance details Defined in Agda.Interaction.InteractionTop Methods readsPrec :: Int -> ReadS (Interval' a) # readList :: ReadS [Interval' a] # readPrec :: ReadPrec (Interval' a) # readListPrec :: ReadPrec [Interval' a] #
Show a => Show (Interval' (Maybe a)) #
Instance details Defined in Agda.Syntax.Position Methods showsPrec :: Int -> Interval' (Maybe a) -> ShowS # show :: Interval' (Maybe a) -> String # showList :: [Interval' (Maybe a)] -> ShowS #
Generic (Interval' a) #
Instance details Defined in Agda.Syntax.Position Associated Types type Rep (Interval' a) :: * -> * # Methods from :: Interval' a -> Rep (Interval' a) x # to :: Rep (Interval' a) x -> Interval' a #
Pretty a => Pretty (Interval' (Maybe a)) #
Instance details Defined in Agda.Syntax.Position Methods pretty :: Interval' (Maybe a) -> Doc # prettyPrec :: Int -> Interval' (Maybe a) -> Doc # prettyList :: [Interval' (Maybe a)] -> Doc #
EmbPrj a => EmbPrj (Interval' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Interval' a -> S Int32 # icod_ :: Interval' a -> S Int32 # value :: Int32 -> R (Interval' a) #
type Rep (Interval' a) #
Instance details Defined in Agda.Syntax.Position type Rep (Interval' a) = D1 (MetaData "Interval'" "Agda.Syntax.Position" "Agda-2.5.4-BdDHVHYPm5JDI57G7c5E26" 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 #

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

Converts a file name and two positions to an interval.

takeI :: String -> Interval' a -> Interval' a #

Extracts the interval corresponding to the given string, assuming that the string starts at the beginning of the given interval.

Precondition: The string must not be too long for the interval.

dropI :: String -> Interval' a -> Interval' a #

Removes the interval corresponding to the given string from the given interval, assuming that the string starts at the beginning of the interval.

Precondition: The string must not be too long for the interval.

getIntervalFile :: Interval' a -> a #

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

iLength :: Interval' a -> Int32 #

The length of an interval.

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

Finds the least interval which covers the arguments.

Precondition: The intervals must point to the same file.

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

Sets the srcFile components of the interval.

Ranges

type Range = Range' SrcFile #

data Range' a #

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

Note the invariant which ranges have to satisfy: rangeInvariant.

Constructors

NoRange
Range !a (Seq IntervalWithoutFile)

Instances

Functor Range' #
Instance details Defined in Agda.Syntax.Position Methods fmap :: (a -> b) -> Range' a -> Range' b # (<$) :: a -> Range' b -> Range' a #
Foldable Range' #
Instance details Defined in Agda.Syntax.Position Methods fold :: Monoid m => Range' m -> m # foldMap :: Monoid m => (a -> m) -> Range' a -> m # foldr :: (a -> b -> b) -> b -> Range' a -> b # foldr' :: (a -> b -> b) -> b -> Range' a -> b # foldl :: (b -> a -> b) -> b -> Range' a -> b # foldl' :: (b -> a -> b) -> b -> Range' a -> b # foldr1 :: (a -> a -> a) -> Range' a -> a # foldl1 :: (a -> a -> a) -> Range' a -> a # toList :: Range' a -> [a] # null :: Range' a -> Bool # length :: Range' a -> Int # elem :: Eq a => a -> Range' a -> Bool # maximum :: Ord a => Range' a -> a # minimum :: Ord a => Range' a -> a # sum :: Num a => Range' a -> a # product :: Num a => Range' a -> a #
Traversable Range' #
Instance details Defined in Agda.Syntax.Position Methods traverse :: Applicative f => (a -> f b) -> Range' a -> f (Range' b) # sequenceA :: Applicative f => Range' (f a) -> f (Range' a) # mapM :: Monad m => (a -> m b) -> Range' a -> m (Range' b) # sequence :: Monad m => Range' (m a) -> m (Range' a) #
KillRange Range #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Range #
SetRange Range #
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> Range -> Range #
HasRange Range #
Instance details Defined in Agda.Syntax.Position Methods getRange :: Range -> Range #
FreshName Range #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadState TCState m => Range -> m Name #
EmbPrj Range #	Ranges are always deserialised as `noRange`.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Range -> S Int32 # icod_ :: Range -> S Int32 # value :: Int32 -> R Range #
PrettyTCM Range #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Range -> TCM Doc #
Subst Term Range #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Range -> Range #
Eq a => Eq (Range' a) #
Instance details Defined in Agda.Syntax.Position Methods (==) :: Range' a -> Range' a -> Bool # (/=) :: Range' a -> Range' a -> Bool #
Data a => Data (Range' a) #
Instance details Defined in Agda.Syntax.Position Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Range' a -> c (Range' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Range' a) # toConstr :: Range' a -> Constr # dataTypeOf :: Range' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Range' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Range' a)) # gmapT :: (forall b. Data b => b -> b) -> Range' a -> Range' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Range' a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Range' a -> r # gmapQ :: (forall d. Data d => d -> u) -> Range' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Range' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Range' a -> m (Range' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Range' a -> m (Range' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Range' a -> m (Range' a) #
Ord a => Ord (Range' a) #
Instance details Defined in Agda.Syntax.Position Methods compare :: Range' a -> Range' a -> Ordering # (<) :: Range' a -> Range' a -> Bool # (<=) :: Range' a -> Range' a -> Bool # (>) :: Range' a -> Range' a -> Bool # (>=) :: Range' a -> Range' a -> Bool # max :: Range' a -> Range' a -> Range' a # min :: Range' a -> Range' a -> Range' a #
Read a => Read (Range' a) #	Note that the grammar implemented by this instance does not necessarily match the current representation of ranges.
Instance details Defined in Agda.Interaction.InteractionTop Methods readsPrec :: Int -> ReadS (Range' a) # readList :: ReadS [Range' a] # readPrec :: ReadPrec (Range' a) # readListPrec :: ReadPrec [Range' a] #
Show a => Show (Range' (Maybe a)) #
Instance details Defined in Agda.Syntax.Position Methods showsPrec :: Int -> Range' (Maybe a) -> ShowS # show :: Range' (Maybe a) -> String # showList :: [Range' (Maybe a)] -> ShowS #
Show a => Show (Range' (Maybe a)) #
Instance details Defined in Agda.Syntax.Position Methods showsPrec :: Int -> Range' (Maybe a) -> ShowS # show :: Range' (Maybe a) -> String # showList :: [Range' (Maybe a)] -> ShowS #
Generic (Range' a) #
Instance details Defined in Agda.Syntax.Position Associated Types type Rep (Range' a) :: * -> * # Methods from :: Range' a -> Rep (Range' a) x # to :: Rep (Range' a) x -> Range' a #
Null (Range' a) #
Instance details Defined in Agda.Syntax.Position Methods empty :: Range' a # null :: Range' a -> Bool #
Pretty a => Pretty (Range' (Maybe a)) #
Instance details Defined in Agda.Syntax.Position Methods pretty :: Range' (Maybe a) -> Doc # prettyPrec :: Int -> Range' (Maybe a) -> Doc # prettyList :: [Range' (Maybe a)] -> Doc #
FreshName (Range, String) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadState TCState m => (Range, String) -> m Name #
type Rep (Range' a) #
Instance details Defined in Agda.Syntax.Position type Rep (Range' a) = D1 (MetaData "Range'" "Agda.Syntax.Position" "Agda-2.5.4-BdDHVHYPm5JDI57G7c5E26" False) (C1 (MetaCons "NoRange" PrefixI False) (U1 :: * -> ) :+: 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 #

Range invariant.

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

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

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

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

Precondition: consecutiveAndSeparated.

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

Converts a file name and an interval to a range.

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

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

rangeFile :: Range -> SrcFile #

The file the range is pointing to.

rightMargin :: Range -> Range #

Conflate a range to its right margin.

noRange :: Range' a #

Ranges between two unknown positions

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

Converts two positions to a range.

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

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

Converts a file name and two positions to a range.

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

The initial position in the range, if any.

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

The initial position in the range, if any.

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

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

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

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

rangeToInterval :: Range' a -> Maybe IntervalWithoutFile #

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

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

Converts a range to an interval, if possible.

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

Returns the shortest continuous range containing the given one.

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

Removes gaps between intervals on the same line.

newtype PrintRange a #

Wrapper to indicate that range should be printed.

Constructors

PrintRange a

Instances

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

class HasRange t where #

Things that have a range are instances of this class.

Minimal complete definition

getRange

Methods

getRange :: t -> Range #

Instances

HasRange Bool #
Instance details Defined in Agda.Syntax.Position Methods getRange :: Bool -> Range #
HasRange Range #
Instance details Defined in Agda.Syntax.Position Methods getRange :: Range -> Range #
HasRange Interval #
Instance details Defined in Agda.Syntax.Position Methods getRange :: Interval -> Range #
HasRange ParseWarning #
Instance details Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseWarning -> Range #
HasRange ParseError #
Instance details Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseError -> Range #
HasRange Layer #
Instance details Defined in Agda.Syntax.Parser.Literate Methods getRange :: Layer -> Range #
HasRange IsMacro #
Instance details Defined in Agda.Syntax.Common Methods getRange :: IsMacro -> Range #
HasRange IsInstance #
Instance details Defined in Agda.Syntax.Common Methods getRange :: IsInstance -> Range #
HasRange Access #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Access -> Range #
HasRange Induction #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Induction -> Range #
HasRange HasEta #
Instance details Defined in Agda.Syntax.Common Methods getRange :: HasEta -> Range #
HasRange TopLevelModuleName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: TopLevelModuleName -> Range #
HasRange QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: QName -> Range #
HasRange Name #
Instance details Defined in Agda.Syntax.Concrete.Name Methods getRange :: Name -> Range #
HasRange AmbiguousQName #	The range of an `AmbiguousQName` is the range of any of its disambiguations (they are the same concrete name).
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: AmbiguousQName -> Range #
HasRange ModuleName #
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: ModuleName -> Range #
HasRange QName #
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: QName -> Range #
HasRange Name #
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: Name -> Range #
HasRange Literal #
Instance details Defined in Agda.Syntax.Literal Methods getRange :: Literal -> Range #
HasRange Token #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods getRange :: Token -> Range #
HasRange Fixity #
Instance details Defined in Agda.Syntax.Fixity Methods getRange :: Fixity -> Range #
HasRange Pragma #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Pragma -> Range #
HasRange ModuleApplication #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: ModuleApplication -> Range #
HasRange Declaration #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Declaration -> Range #
HasRange AsName #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: AsName -> Range #
HasRange LamClause #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamClause -> Range #
HasRange WhereClause #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: WhereClause -> Range #
HasRange RHS #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: RHS -> Range #
HasRange LHSCore #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LHSCore -> Range #
HasRange LHS #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LHS -> Range #
HasRange TypedBinding #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: TypedBinding -> Range #
HasRange BoundName #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: BoundName -> Range #
HasRange TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: TypedBindings -> Range #
HasRange LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range #
HasRange DoStmt #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: DoStmt -> Range #
HasRange Pattern #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Pattern -> Range #
HasRange Expr #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Expr -> Range #
HasRange ModuleAssignment #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: ModuleAssignment -> Range #
HasRange AbstractName #
Instance details Defined in Agda.Syntax.Scope.Base Methods getRange :: AbstractName -> Range #
HasRange ConPatInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: ConPatInfo -> Range #
HasRange PatInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: PatInfo -> Range #
HasRange LHSInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: LHSInfo -> Range #
HasRange MutualInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: MutualInfo -> Range #
HasRange DeclInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: DeclInfo -> Range #
HasRange DefInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: DefInfo -> Range #
HasRange LetInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: LetInfo -> Range #
HasRange ModuleInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: ModuleInfo -> Range #
HasRange AppInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: AppInfo -> Range #
HasRange ExprInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: ExprInfo -> Range #
HasRange MetaInfo #
Instance details Defined in Agda.Syntax.Info Methods getRange :: MetaInfo -> Range #
HasRange Clause #
Instance details Defined in Agda.Syntax.Internal Methods getRange :: Clause -> Range #
HasRange ConHead #
Instance details Defined in Agda.Syntax.Internal Methods getRange :: ConHead -> Range #
HasRange LHS #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LHS -> Range #
HasRange SpineLHS #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: SpineLHS -> Range #
HasRange RHS #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: RHS -> Range #
HasRange WhereDeclarations #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: WhereDeclarations -> Range #
HasRange TypedBinding #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: TypedBinding -> Range #
HasRange TypedBindings #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: TypedBindings -> Range #
HasRange LamBinding #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LamBinding -> Range #
HasRange LetBinding #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LetBinding -> Range #
HasRange Declaration #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Declaration -> Range #
HasRange Expr #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Expr -> Range #
HasRange BindName #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: BindName -> Range #
HasRange DeclarationWarning #
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods getRange :: DeclarationWarning -> Range #
HasRange DeclarationException #
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods getRange :: DeclarationException -> Range #
HasRange NiceDeclaration #
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods getRange :: NiceDeclaration -> Range #
HasRange TCErr #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: TCErr -> Range #
HasRange TCWarning #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: TCWarning -> Range #
HasRange Call #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Call -> Range #
HasRange CompilerPragma #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: CompilerPragma -> Range #
HasRange MetaInfo #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: MetaInfo -> Range #
HasRange MetaVariable #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: MetaVariable -> Range #
HasRange Constraint #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Constraint -> Range #
HasRange ProblemConstraint #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: ProblemConstraint -> Range #
HasRange Item #
Instance details Defined in Agda.TypeChecking.Positivity Methods getRange :: Item -> Range #
HasRange HaskellPragma #
Instance details Defined in Agda.Compiler.MAlonzo.Pragmas Methods getRange :: HaskellPragma -> Range #
HasRange a => HasRange [a] #	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 #
HasRange a => HasRange (Maybe a) #
Instance details Defined in Agda.Syntax.Position Methods getRange :: Maybe a -> Range #
HasRange a => HasRange (NonemptyList a) #	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 :: NonemptyList a -> Range #
HasRange a => HasRange (PrintRange a) #
Instance details Defined in Agda.Syntax.Position Methods getRange :: PrintRange a -> Range #
HasRange a => HasRange (MaybePlaceholder a) #
Instance details Defined in Agda.Syntax.Common Methods getRange :: MaybePlaceholder a -> Range #
HasRange (Ranged a) #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Ranged a -> Range #
HasRange a => HasRange (Dom a) #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Dom a -> Range #
HasRange a => HasRange (Arg a) #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Arg a -> Range #
HasRange a => HasRange (WithOrigin a) #
Instance details Defined in Agda.Syntax.Common Methods getRange :: WithOrigin a -> Range #
HasRange a => HasRange (WithHiding a) #
Instance details Defined in Agda.Syntax.Common Methods getRange :: WithHiding a -> Range #
HasRange a => HasRange (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: FieldAssignment' a -> Range #
HasRange e => HasRange (OpApp e) #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: OpApp e -> Range #
IsExpr e => HasRange (ExprView e) #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser Methods getRange :: ExprView e -> Range #
HasRange (Pattern' e) #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Pattern' e -> Range #
HasRange (LHSCore' e) #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LHSCore' e -> Range #
HasRange a => HasRange (Clause' a) #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Clause' a -> Range #
HasRange a => HasRange (Closure a) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Closure a -> Range #
(HasRange a, HasRange b) => HasRange (Either a b) #
Instance details Defined in Agda.Syntax.Position Methods getRange :: Either a b -> Range #
(HasRange a, HasRange b) => HasRange (a, b) #	Precondition: The ranges of the tuple elements must point to the same file (or be empty).
Instance details Defined in Agda.Syntax.Position Methods getRange :: (a, b) -> Range #
(HasRange a, HasRange b) => HasRange (Renaming' a b) #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Renaming' a b -> Range #
(HasRange a, HasRange b) => HasRange (ImportedName' a b) #
Instance details Defined in Agda.Syntax.Common Methods getRange :: ImportedName' a b -> Range #
(HasRange a, HasRange b) => HasRange (Using' a b) #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Using' a b -> Range #
(HasRange a, HasRange b) => HasRange (ImportDirective' a b) #
Instance details Defined in Agda.Syntax.Common Methods getRange :: ImportDirective' a b -> Range #
HasRange a => HasRange (Named name a) #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Named name a -> Range #
(HasRange a, HasRange b, HasRange c) => HasRange (a, b, c) #	Precondition: The ranges of the tuple elements must point to the same file (or be empty).
Instance details Defined in Agda.Syntax.Position Methods getRange :: (a, b, c) -> Range #
(HasRange a, HasRange b, HasRange c, HasRange d) => HasRange (a, b, c, d) #	Precondition: The ranges of the tuple elements must point to the same file (or be empty).
Instance details Defined in Agda.Syntax.Position Methods getRange :: (a, b, c, d) -> Range #
(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e) => HasRange (a, b, c, d, e) #	Precondition: The ranges of the tuple elements must point to the same file (or be empty).
Instance details Defined in Agda.Syntax.Position Methods getRange :: (a, b, c, d, e) -> Range #
(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f) => HasRange (a, b, c, d, e, f) #	Precondition: The ranges of the tuple elements must point to the same file (or be empty).
Instance details Defined in Agda.Syntax.Position Methods getRange :: (a, b, c, d, e, f) -> Range #
(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f, HasRange g) => HasRange (a, b, c, d, e, f, g) #	Precondition: The ranges of the tuple elements must point to the same file (or be empty).
Instance details Defined in Agda.Syntax.Position Methods getRange :: (a, b, c, d, e, f, g) -> Range #

class HasRange t => SetRange t where #

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

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

Minimal complete definition

setRange

Methods

setRange :: Range -> t -> t #

Instances

SetRange Range #
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> Range -> Range #
SetRange TopLevelModuleName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> TopLevelModuleName -> TopLevelModuleName #
SetRange QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> QName -> QName #
SetRange Name #
Instance details Defined in Agda.Syntax.Concrete.Name Methods setRange :: Range -> Name -> Name #
SetRange ModuleName #
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> ModuleName -> ModuleName #
SetRange QName #
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> QName -> QName #
SetRange Name #
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> Name -> Name #
SetRange Literal #
Instance details Defined in Agda.Syntax.Literal Methods setRange :: Range -> Literal -> Literal #
SetRange TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods setRange :: Range -> TypedBindings -> TypedBindings #
SetRange Pattern #
Instance details Defined in Agda.Syntax.Concrete Methods setRange :: Range -> Pattern -> Pattern #
SetRange AbstractName #
Instance details Defined in Agda.Syntax.Scope.Base Methods setRange :: Range -> AbstractName -> AbstractName #
SetRange ConPatInfo #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> ConPatInfo -> ConPatInfo #
SetRange PatInfo #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> PatInfo -> PatInfo #
SetRange DeclInfo #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> DeclInfo -> DeclInfo #
SetRange DefInfo #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> DefInfo -> DefInfo #
SetRange ModuleInfo #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> ModuleInfo -> ModuleInfo #
SetRange ConHead #
Instance details Defined in Agda.Syntax.Internal Methods setRange :: Range -> ConHead -> ConHead #
SetRange BindName #
Instance details Defined in Agda.Syntax.Abstract Methods setRange :: Range -> BindName -> BindName #
SetRange MetaInfo #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods setRange :: Range -> MetaInfo -> MetaInfo #
SetRange MetaVariable #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods setRange :: Range -> MetaVariable -> MetaVariable #
SetRange a => SetRange [a] #
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> [a] -> [a] #
SetRange a => SetRange (PrintRange a) #
Instance details Defined in Agda.Syntax.Position Methods setRange :: Range -> PrintRange a -> PrintRange a #
SetRange a => SetRange (Arg a) #
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Arg a -> Arg a #
SetRange a => SetRange (WithOrigin a) #
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> WithOrigin a -> WithOrigin a #
SetRange a => SetRange (WithHiding a) #
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> WithHiding a -> WithHiding a #
SetRange (Pattern' a) #
Instance details Defined in Agda.Syntax.Abstract Methods setRange :: Range -> Pattern' a -> Pattern' a #
SetRange a => SetRange (Named name a) #
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Named name a -> Named name a #

class KillRange a where #

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

Minimal complete definition

killRange

Methods

killRange :: KillRangeT a #

Instances

KillRange Bool #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Bool #
KillRange Int #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Int #
KillRange Integer #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Integer #
KillRange () #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT () #
KillRange Void #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Void #
KillRange String #	Overlaps with `KillRange [a]`.
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT String #
KillRange Range #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Range #
KillRange Permutation #
Instance details Defined in Agda.Utils.Permutation Methods killRange :: KillRangeT Permutation #
KillRange Fixity' #
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT Fixity' #
KillRange InteractionId #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT InteractionId #
KillRange NameId #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT NameId #
KillRange IsMacro #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsMacro #
KillRange IsInstance #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsInstance #
KillRange IsAbstract #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsAbstract #
KillRange Access #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Access #
KillRange ProjOrigin #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT ProjOrigin #
KillRange ConOrigin #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT ConOrigin #
KillRange ArgInfo #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT ArgInfo #
KillRange Origin #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Origin #
KillRange Relevance #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Relevance #
KillRange Quantity #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Quantity #
KillRange Modality #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Modality #
KillRange Hiding #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Hiding #
KillRange Induction #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Induction #
KillRange HasEta #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT HasEta #
KillRange Delayed #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Delayed #
KillRange TopLevelModuleName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT TopLevelModuleName #
KillRange QName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT QName #
KillRange Name #
Instance details Defined in Agda.Syntax.Concrete.Name Methods killRange :: KillRangeT Name #
KillRange GenPart #
Instance details Defined in Agda.Syntax.Notation Methods killRange :: KillRangeT GenPart #
KillRange AmbiguousQName #
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT AmbiguousQName #
KillRange ModuleName #
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT ModuleName #
KillRange QName #
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT QName #
KillRange Name #
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT Name #
KillRange Literal #
Instance details Defined in Agda.Syntax.Literal Methods killRange :: KillRangeT Literal #
KillRange Compiled #
Instance details Defined in Agda.Syntax.Treeless Methods killRange :: KillRangeT Compiled #
KillRange Fixity #
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT Fixity #
KillRange Occurrence #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods killRange :: KillRangeT Occurrence #
KillRange Pragma #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Pragma #
KillRange ModuleApplication #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT ModuleApplication #
KillRange Declaration #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Declaration #
KillRange AsName #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT AsName #
KillRange LamClause #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamClause #
KillRange WhereClause #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT WhereClause #
KillRange RHS #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT RHS #
KillRange LHS #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LHS #
KillRange TypedBinding #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT TypedBinding #
KillRange BoundName #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT BoundName #
KillRange TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT TypedBindings #
KillRange LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamBinding #
KillRange DoStmt #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT DoStmt #
KillRange Pattern #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Pattern #
KillRange Expr #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Expr #
KillRange ModuleAssignment #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT ModuleAssignment #
KillRange ScopeInfo #
Instance details Defined in Agda.Syntax.Scope.Base Methods killRange :: KillRangeT ScopeInfo #
KillRange ConPatInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ConPatInfo #
KillRange PatInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT PatInfo #
KillRange LHSInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT LHSInfo #
KillRange MutualInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT MutualInfo #
KillRange DeclInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT DeclInfo #
KillRange DefInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT DefInfo #
KillRange LetInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT LetInfo #
KillRange ModuleInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ModuleInfo #
KillRange AppInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT AppInfo #
KillRange ExprInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ExprInfo #
KillRange MetaInfo #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT MetaInfo #
KillRange Substitution #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Substitution #
KillRange ConPatternInfo #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT ConPatternInfo #
KillRange DBPatVar #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT DBPatVar #
KillRange PatOrigin #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT PatOrigin #
KillRange Clause #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Clause #
KillRange LevelAtom #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT LevelAtom #
KillRange PlusLevel #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT PlusLevel #
KillRange Level #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Level #
KillRange Sort #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Sort #
KillRange Term #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Term #
KillRange ConHead #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT ConHead #
KillRange CompiledClauses #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT CompiledClauses #
KillRange LHS #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LHS #
KillRange SpineLHS #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT SpineLHS #
KillRange RHS #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT RHS #
KillRange WhereDeclarations #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT WhereDeclarations #
KillRange ProblemEq #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ProblemEq #
KillRange TypedBinding #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT TypedBinding #
KillRange TypedBindings #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT TypedBindings #
KillRange LamBinding #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LamBinding #
KillRange LetBinding #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LetBinding #
KillRange ModuleApplication #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ModuleApplication #
KillRange Declaration #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Declaration #
KillRange ScopeCopyInfo #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ScopeCopyInfo #
KillRange Expr #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Expr #
KillRange BindName #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT BindName #
KillRange MutualId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT MutualId #
KillRange TermHead #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT TermHead #
KillRange Defn #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Defn #
KillRange FunctionFlag #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT FunctionFlag #
KillRange EtaEquality #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT EtaEquality #
KillRange ProjLams #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT ProjLams #
KillRange Projection #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Projection #
KillRange ExtLamInfo #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT ExtLamInfo #
KillRange CompiledRepresentation #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT CompiledRepresentation #
KillRange IsForced #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT IsForced #
KillRange Polarity #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Polarity #
KillRange Definition #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Definition #
KillRange RewriteRule #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT RewriteRule #
KillRange NLPType #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT NLPType #
KillRange NLPat #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT NLPat #
KillRange DisplayTerm #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT DisplayTerm #
KillRange DisplayForm #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT DisplayForm #
KillRange Section #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Section #
KillRange RewriteRuleMap #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT RewriteRuleMap #
KillRange Definitions #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Definitions #
KillRange Sections #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Sections #
KillRange Signature #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Signature #
KillRange a => KillRange [a] #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT [a] #
KillRange a => KillRange (Maybe a) #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Maybe a) #
(Ord a, KillRange a) => KillRange (Set a) #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Set a) #
KillRange a => KillRange (NonemptyList a) #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (NonemptyList a) #
KillRange a => KillRange (PrintRange a) #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (PrintRange a) #
KillRange a => KillRange (Drop a) #
Instance details Defined in Agda.Utils.Permutation Methods killRange :: KillRangeT (Drop a) #
KillRange m => KillRange (TerminationCheck m) #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (TerminationCheck m) #
KillRange a => KillRange (MaybePlaceholder a) #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (MaybePlaceholder a) #
KillRange (Ranged a) #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Ranged a) #
KillRange a => KillRange (Dom a) #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Dom a) #
KillRange a => KillRange (Arg a) #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Arg a) #
KillRange a => KillRange (WithOrigin a) #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (WithOrigin a) #
KillRange a => KillRange (WithHiding a) #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (WithHiding a) #
KillRange x => KillRange (ThingWithFixity x) #
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) #
KillRange a => KillRange (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (FieldAssignment' a) #
KillRange e => KillRange (OpApp e) #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (OpApp e) #
KillRange a => KillRange (Pattern' a) #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Pattern' a) #
KillRange a => KillRange (Blocked a) #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Blocked a) #
KillRange a => KillRange (Tele a) #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Tele a) #
KillRange a => KillRange (Type' a) #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Type' a) #
KillRange a => KillRange (Abs a) #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Abs a) #
KillRange a => KillRange (Elim' a) #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Elim' a) #
KillRange c => KillRange (Case c) #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (Case c) #
KillRange c => KillRange (WithArity c) #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (WithArity c) #
KillRange e => KillRange (Pattern' e) #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Pattern' e) #
KillRange e => KillRange (LHSCore' e) #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (LHSCore' e) #
KillRange a => KillRange (Clause' a) #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Clause' a) #
KillRange c => KillRange (FunctionInverse' c) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (FunctionInverse' c) #
KillRange a => KillRange (Open a) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (Open a) #
(KillRange a, KillRange b) => KillRange (Either a b) #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Either a b) #
(KillRange a, KillRange b) => KillRange (a, b) #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (a, b) #
KillRange a => KillRange (Map k a) #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Map k a) #
(KillRange a, KillRange b) => KillRange (Renaming' a b) #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Renaming' a b) #
(KillRange a, KillRange b) => KillRange (ImportedName' a b) #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportedName' a b) #
(KillRange a, KillRange b) => KillRange (Using' a b) #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Using' a b) #
(KillRange a, KillRange b) => KillRange (ImportDirective' a b) #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportDirective' a b) #
(KillRange name, KillRange a) => KillRange (Named name a) #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Named name a) #
(KillRange a, KillRange b, KillRange c) => KillRange (a, b, c) #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (a, b, c) #
(KillRange a, KillRange b, KillRange c, KillRange d) => KillRange (a, b, c, d) #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (a, b, c, d) #

type KillRangeT a = a -> a #

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

Remove ranges in keys and values of a map.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

beginningOf :: Range -> Range #

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

beginningOfFile :: Range -> Range #

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

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

Interleaves two streams of ranged elements

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