| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Position
Description
Position information for syntax. Crucial for giving good error messages.
Synopsis
- type Position = Position' SrcFile
- type PositionWithoutFile = Position' ()
- data Position' a = Pn {}
- type SrcFile = Maybe RangeFile
- data RangeFile = RangeFile {}
- mkRangeFile :: AbsolutePath -> Maybe (TopLevelModuleName' Range) -> RangeFile
- positionInvariant :: Position' a -> Bool
- startPos :: Maybe RangeFile -> Position
- movePos :: Position' a -> Char -> Position' a
- movePosByString :: Foldable t => Position' a -> t Char -> Position' a
- backupPos :: Position' a -> Position' a
- startPos' :: a -> Position' a
- type Interval = Interval' SrcFile
- type IntervalWithoutFile = Interval' ()
- data Interval' a = Interval {}
- 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
- rangeModule' :: Range -> Maybe (Maybe (TopLevelModuleName' Range))
- rangeModule :: Range -> Maybe (TopLevelModuleName' Range)
- rightMargin :: Range -> Range
- noRange :: Range' a
- posToRange :: Position' a -> Position' a -> Range' a
- posToRange' :: a -> PositionWithoutFile -> PositionWithoutFile -> Range' a
- rStart :: Range' a -> Maybe (Position' a)
- rStart' :: Range' a -> Maybe PositionWithoutFile
- rEnd :: Range' a -> Maybe (Position' a)
- rEnd' :: Range' a -> Maybe PositionWithoutFile
- rangeToInterval :: Range' a -> Maybe IntervalWithoutFile
- rangeToIntervalWithFile :: Range' a -> Maybe (Interval' a)
- continuous :: Range' a -> Range' a
- continuousPerLine :: Ord a => Range' a -> Range' a
- newtype PrintRange a = PrintRange a
- class HasRange a where
- class HasRange a => SetRange a where
- class KillRange a where
- killRange :: KillRangeT a
- type KillRangeT a = a -> a
- killRangeMap :: (KillRange k, KillRange v) => KillRangeT (Map k v)
- class KILLRANGE t (b :: Bool) where
- killRangeN :: t -> t
- withRangeOf :: (SetRange t, HasRange u) => t -> u -> t
- fuseRange :: (HasRange u, HasRange t) => u -> t -> Range
- fuseRanges :: Ord a => Range' a -> Range' a -> Range' a
- beginningOf :: Range -> Range
- beginningOfFile :: Range -> Range
- interleaveRanges :: HasRange a => [a] -> [a] -> ([a], [(a, a)])
Positions
type PositionWithoutFile = Position' () 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 | |
Instances
| Pretty PositionWithoutFile Source # | |||||
Defined in Agda.Syntax.Common.Pretty Methods pretty :: PositionWithoutFile -> Doc Source # prettyPrec :: Int -> PositionWithoutFile -> Doc Source # prettyList :: [PositionWithoutFile] -> Doc Source # | |||||
| NFData Position Source # | |||||
Defined in Agda.Syntax.Position | |||||
| NFData PositionWithoutFile Source # | |||||
Defined in Agda.Syntax.Position Methods rnf :: PositionWithoutFile -> () | |||||
| Functor Position' Source # | |||||
| Foldable Position' Source # | |||||
Defined in Agda.Syntax.Position Methods fold :: Monoid m => Position' m -> m foldMap :: Monoid m => (a -> m) -> Position' a -> m foldMap' :: Monoid m => (a -> m) -> Position' a -> m foldr :: (a -> b -> b) -> b -> Position' a -> b foldr' :: (a -> b -> b) -> b -> Position' a -> b foldl :: (b -> a -> b) -> b -> Position' a -> b foldl' :: (b -> a -> b) -> b -> Position' a -> b foldr1 :: (a -> a -> a) -> Position' a -> a foldl1 :: (a -> a -> a) -> Position' a -> a elem :: Eq a => a -> Position' a -> Bool maximum :: Ord a => Position' a -> a minimum :: Ord a => Position' a -> a | |||||
| Traversable Position' Source # | |||||
| EncodeTCM (Position' ()) Source # | |||||
| Pretty a => Pretty (Position' (Maybe a)) Source # | |||||
| EmbPrj a => EmbPrj (Position' a) Source # | |||||
| Generic (Position' a) Source # | |||||
Defined in Agda.Syntax.Position Associated Types
| |||||
| Read a => Read (Position' a) | |||||
Defined in Agda.Interaction.Base | |||||
| Show a => Show (Position' a) Source # | |||||
| Eq a => Eq (Position' a) Source # | |||||
| Ord a => Ord (Position' a) Source # | |||||
Defined in Agda.Syntax.Position | |||||
| ToJSON (Position' ()) Source # | |||||
Defined in Agda.Interaction.JSONTop | |||||
| type Rep (Position' a) Source # | |||||
Defined in Agda.Syntax.Position type Rep (Position' a) = D1 ('MetaData "Position'" "Agda.Syntax.Position" "Agda-2.6.20240714-inplace" '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)))) | |||||
Constructors
| RangeFile | |
Fields
| |
Instances
mkRangeFile :: AbsolutePath -> Maybe (TopLevelModuleName' Range) -> RangeFile Source #
A smart constructor for RangeFile.
positionInvariant :: Position' a -> Bool Source #
startPos :: Maybe RangeFile -> Position Source #
The first position in a file: position 1, line 1, column 1.
movePos :: Position' a -> Char -> Position' a Source #
Advance the position by one character.
A newline character ('n') moves the position to the first
character in the next line. Any other character moves the
position to the next column.
movePosByString :: Foldable t => Position' a -> t Char -> Position' a Source #
Advance the position by a string.
movePosByString = foldl' movePos
backupPos :: Position' a -> Position' a Source #
Backup the position by one character.
Precondition: The character must not be 'n'.
Intervals
type IntervalWithoutFile = Interval' () Source #
An interval. The iEnd position is not included in the interval.
Note the invariant which intervals have to satisfy: intervalInvariant.
Instances
| Pretty IntervalWithoutFile Source # | |||||
Defined in Agda.Syntax.Common.Pretty Methods pretty :: IntervalWithoutFile -> Doc Source # prettyPrec :: Int -> IntervalWithoutFile -> Doc Source # prettyList :: [IntervalWithoutFile] -> Doc Source # | |||||
| HasRange Interval Source # | |||||
| NFData Interval Source # | |||||
Defined in Agda.Syntax.Position | |||||
| NFData IntervalWithoutFile Source # | |||||
Defined in Agda.Syntax.Position Methods rnf :: IntervalWithoutFile -> () | |||||
| Functor Interval' Source # | |||||
| Foldable Interval' Source # | |||||
Defined in Agda.Syntax.Position Methods fold :: Monoid m => Interval' m -> m foldMap :: Monoid m => (a -> m) -> Interval' a -> m foldMap' :: Monoid m => (a -> m) -> Interval' a -> m foldr :: (a -> b -> b) -> b -> Interval' a -> b foldr' :: (a -> b -> b) -> b -> Interval' a -> b foldl :: (b -> a -> b) -> b -> Interval' a -> b foldl' :: (b -> a -> b) -> b -> Interval' a -> b foldr1 :: (a -> a -> a) -> Interval' a -> a foldl1 :: (a -> a -> a) -> Interval' a -> a elem :: Eq a => a -> Interval' a -> Bool maximum :: Ord a => Interval' a -> a minimum :: Ord a => Interval' a -> a | |||||
| Traversable Interval' Source # | |||||
| Pretty a => Pretty (Interval' (Maybe a)) Source # | |||||
| EmbPrj a => EmbPrj (Interval' a) Source # | |||||
| Generic (Interval' a) Source # | |||||
Defined in Agda.Syntax.Position Associated Types
| |||||
| Read a => Read (Interval' a) | |||||
Defined in Agda.Interaction.Base | |||||
| Show a => Show (Interval' a) Source # | |||||
| Eq a => Eq (Interval' a) Source # | |||||
| Ord a => Ord (Interval' a) Source # | |||||
Defined in Agda.Syntax.Position | |||||
| type Rep (Interval' a) Source # | |||||
Defined in Agda.Syntax.Position type Rep (Interval' a) = D1 ('MetaData "Interval'" "Agda.Syntax.Position" "Agda-2.6.20240714-inplace" '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.
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
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
| EncodeTCM Range Source # | |||||
| Pretty TopLevelModuleName Source # | |||||
Defined in Agda.Syntax.TopLevelModuleName Methods pretty :: TopLevelModuleName -> Doc Source # prettyPrec :: Int -> TopLevelModuleName -> Doc Source # prettyList :: [TopLevelModuleName] -> Doc Source # | |||||
| HasRange Range Source # | |||||
| KillRange Range Source # | |||||
Defined in Agda.Syntax.Position Methods | |||||
| SetRange Range Source # | |||||
| FreshName Range Source # | |||||
Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => Range -> m Name Source # | |||||
| PrettyTCM Range Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
| PrettyTCM TopLevelModuleName Source # | |||||
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TopLevelModuleName -> m Doc Source # | |||||
| EmbPrj Range Source # | Ranges are always deserialised as | ||||
| EmbPrj TopLevelModuleName Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: TopLevelModuleName -> S Int32 Source # icod_ :: TopLevelModuleName -> S Int32 Source # value :: Int32 -> R TopLevelModuleName Source # | |||||
| Subst Range Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source # | |||||
| Sized TopLevelModuleName Source # | |||||
Defined in Agda.Syntax.TopLevelModuleName | |||||
| Functor Range' Source # | |||||
| Foldable Range' Source # | |||||
Defined in Agda.Syntax.Position Methods fold :: Monoid m => Range' m -> m foldMap :: Monoid m => (a -> m) -> Range' a -> m foldMap' :: Monoid m => (a -> m) -> Range' a -> m foldr :: (a -> b -> b) -> b -> Range' a -> b foldr' :: (a -> b -> b) -> b -> Range' a -> b foldl :: (b -> a -> b) -> b -> Range' a -> b foldl' :: (b -> a -> b) -> b -> Range' a -> b foldr1 :: (a -> a -> a) -> Range' a -> a foldl1 :: (a -> a -> a) -> Range' a -> a elem :: Eq a => a -> Range' a -> Bool maximum :: Ord a => Range' a -> a | |||||
| Traversable Range' Source # | |||||
| ToJSON Range Source # | |||||
Defined in Agda.Interaction.JSONTop | |||||
| LensClosure MetaInfo Range Source # | |||||
Defined in Agda.TypeChecking.Monad.Base | |||||
| LensClosure MetaVariable Range Source # | |||||
Defined in Agda.TypeChecking.Monad.Base Methods | |||||
| Pretty a => Pretty (Range' (Maybe a)) Source # | |||||
| HasRange (TopLevelModuleName' Range) Source # | |||||
Defined in Agda.Syntax.Position | |||||
| KillRange (TopLevelModuleName' Range) Source # | |||||
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (TopLevelModuleName' Range) Source # | |||||
| SetRange (TopLevelModuleName' Range) Source # | |||||
Defined in Agda.Syntax.Position Methods setRange :: Range -> TopLevelModuleName' Range -> TopLevelModuleName' Range Source # | |||||
| Null (Range' a) Source # | |||||
| NFData a => NFData (Range' a) Source # | |||||
Defined in Agda.Syntax.Position | |||||
| Eq a => Monoid (Range' a) Source # | |||||
| Eq a => Semigroup (Range' a) Source # | |||||
| Generic (Range' a) Source # | |||||
Defined in Agda.Syntax.Position Associated Types
| |||||
| Read a => Read (Range' a) | Note that the grammar implemented by this instance does not necessarily match the current representation of ranges. | ||||
Defined in Agda.Interaction.Base | |||||
| Show a => Show (Range' a) Source # | |||||
| Eq a => Eq (Range' a) Source # | |||||
| Ord a => Ord (Range' a) Source # | |||||
Defined in Agda.Syntax.Position | |||||
| FreshName (Range, String) Source # | |||||
Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => (Range, String) -> m Name Source # | |||||
| type SubstArg Range Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
| type Rep (Range' a) Source # | |||||
Defined in Agda.Syntax.Position type Rep (Range' a) = D1 ('MetaData "Range'" "Agda.Syntax.Position" "Agda-2.6.20240714-inplace" '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).
rangeModule' :: Range -> Maybe (Maybe (TopLevelModuleName' Range)) Source #
rangeModule :: Range -> Maybe (TopLevelModuleName' Range) Source #
The range's top-level module name, if any.
rightMargin :: Range -> Range Source #
Conflate a range to its right margin.
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.
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
| (Pretty a, HasRange a) => Pretty (PrintRange a) Source # | |
Defined in Agda.Syntax.Common.Pretty Methods pretty :: PrintRange a -> Doc Source # prettyPrec :: Int -> PrintRange a -> Doc Source # prettyList :: [PrintRange a] -> Doc Source # | |
| HasRange a => HasRange (PrintRange a) Source # | |
Defined in Agda.Syntax.Position Methods getRange :: PrintRange a -> Range Source # | |
| KillRange a => KillRange (PrintRange a) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (PrintRange a) Source # | |
| SetRange a => SetRange (PrintRange a) Source # | |
Defined in Agda.Syntax.Position Methods setRange :: Range -> PrintRange a -> PrintRange a Source # | |
| Eq a => Eq (PrintRange a) Source # | |
Defined in Agda.Syntax.Position | |
| Ord a => Ord (PrintRange a) Source # | |
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 | |
class HasRange a where Source #
Things that have a range are instances of this class.
Minimal complete definition
Nothing
Methods
Instances
| HasRange HaskellPragma Source # | |
Defined in Agda.Compiler.MAlonzo.Pragmas Methods getRange :: HaskellPragma -> Range Source # | |
| HasRange BindName Source # | |
| HasRange Declaration Source # | |
Defined in Agda.Syntax.Abstract Methods getRange :: Declaration -> Range Source # | |
| HasRange Expr Source # | |
| HasRange LHS Source # | |
| HasRange LamBinding Source # | |
Defined in Agda.Syntax.Abstract Methods getRange :: LamBinding -> Range Source # | |
| HasRange LetBinding Source # | |
Defined in Agda.Syntax.Abstract Methods getRange :: LetBinding -> Range Source # | |
| HasRange RHS Source # | |
| HasRange SpineLHS Source # | |
| HasRange TypedBinding Source # | |
Defined in Agda.Syntax.Abstract Methods getRange :: TypedBinding -> Range Source # | |
| HasRange WhereDeclarations Source # | |
Defined in Agda.Syntax.Abstract Methods getRange :: WhereDeclarations -> Range Source # | |
| HasRange AmbiguousQName Source # | The range of an |
Defined in Agda.Syntax.Abstract.Name Methods getRange :: AmbiguousQName -> Range Source # | |
| HasRange ModuleName Source # | |
Defined in Agda.Syntax.Abstract.Name Methods getRange :: ModuleName -> Range Source # | |
| HasRange Name Source # | |
| HasRange QName Source # | |
| HasRange Access Source # | |
| HasRange Annotation Source # | |
Defined in Agda.Syntax.Common Methods getRange :: Annotation -> Range Source # | |
| HasRange ArgInfo Source # | |
| HasRange Cohesion Source # | |
| HasRange Erased Source # | |
| HasRange Fixity Source # | |
| HasRange Hiding Source # | |
| HasRange IsInstance Source # | |
Defined in Agda.Syntax.Common Methods getRange :: IsInstance -> Range Source # | |
| HasRange IsMacro Source # | |
| HasRange Modality Source # | |
| HasRange NotationPart Source # | |
Defined in Agda.Syntax.Common Methods getRange :: NotationPart -> Range Source # | |
| HasRange Origin Source # | |
| HasRange PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods getRange :: PatternOrCopattern -> Range Source # | |
| HasRange Q0Origin Source # | |
| HasRange Q1Origin Source # | |
| HasRange Quantity Source # | |
| HasRange QωOrigin Source # | |
| HasRange Relevance Source # | |
| HasRange Induction Source # | |
| HasRange KwRange Source # | |
| HasRange AsName Source # | |
| HasRange Binder Source # | |
| HasRange BoundName Source # | |
| HasRange Declaration Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: Declaration -> Range Source # | |
| HasRange DoStmt Source # | |
| HasRange Expr Source # | |
| HasRange LHS Source # | |
| HasRange LHSCore Source # | |
| HasRange LamBinding Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range Source # | |
| HasRange LamClause Source # | |
| HasRange ModuleApplication Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: ModuleApplication -> Range Source # | |
| HasRange ModuleAssignment Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: ModuleAssignment -> Range Source # | |
| HasRange Pattern Source # | |
| HasRange Pragma Source # | |
| HasRange RHS Source # | |
| HasRange RecordDirective Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: RecordDirective -> Range Source # | |
| HasRange TypedBinding Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: TypedBinding -> Range Source # | |
| HasRange WhereClause Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: WhereClause -> Range Source # | |
| HasRange Attribute Source # | |
| HasRange DeclarationException Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationException -> Range Source # | |
| HasRange DeclarationException' Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Errors Methods | |
| HasRange DeclarationWarning Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationWarning -> Range Source # | |
| HasRange DeclarationWarning' Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationWarning' -> Range Source # | |
| HasRange NiceDeclaration Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Types Methods getRange :: NiceDeclaration -> Range Source # | |
| HasRange Name Source # | |
| HasRange QName Source # | |
| HasRange AppInfo Source # | |
| HasRange ConPatInfo Source # | |
Defined in Agda.Syntax.Info Methods getRange :: ConPatInfo -> Range Source # | |
| HasRange DeclInfo Source # | |
| HasRange ExprInfo Source # | |
| HasRange LHSInfo Source # | |
| HasRange LetInfo Source # | |
| HasRange MetaInfo Source # | |
| HasRange ModuleInfo Source # | |
Defined in Agda.Syntax.Info Methods getRange :: ModuleInfo -> Range Source # | |
| HasRange MutualInfo Source # | |
Defined in Agda.Syntax.Info Methods getRange :: MutualInfo -> Range Source # | |
| HasRange PatInfo Source # | |
| HasRange Clause Source # | |
| HasRange ConHead Source # | |
| HasRange Attr Source # | |
| HasRange Layer Source # | |
| HasRange ParseError Source # | |
Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseError -> Range Source # | |
| HasRange ParseWarning Source # | |
Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseWarning -> Range Source # | |
| HasRange Token Source # | |
| HasRange Interval Source # | |
| HasRange Range Source # | |
| HasRange AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Methods getRange :: AbstractName -> Range Source # | |
| HasRange RawTopLevelModuleName Source # | |
Defined in Agda.Syntax.TopLevelModuleName Methods | |
| HasRange Call Source # | |
| HasRange CallInfo Source # | |
| HasRange CompilerPragma Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods getRange :: CompilerPragma -> Range Source # | |
| HasRange Constraint Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Constraint -> Range Source # | |
| HasRange MetaInfo Source # | |
| HasRange MetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods getRange :: MetaVariable -> Range Source # | |
| HasRange ProblemConstraint Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods getRange :: ProblemConstraint -> Range Source # | |
| HasRange TCErr Source # | |
| HasRange TCWarning Source # | |
| HasRange Item Source # | |
| HasRange () Source # | |
Defined in Agda.Syntax.Position | |
| HasRange Bool Source # | |
Defined in Agda.Syntax.Position | |
| HasRange a => HasRange (Binder' a) Source # | |
| HasRange a => HasRange (Clause' a) Source # | |
| HasRange (LHSCore' e) Source # | |
| HasRange (Pattern' e) Source # | |
| HasRange a => HasRange (Arg a) Source # | |
| HasRange a => HasRange (HasEta' a) Source # | |
| HasRange a => HasRange (MaybePlaceholder a) Source # | |
Defined in Agda.Syntax.Common Methods getRange :: MaybePlaceholder a -> Range Source # | |
| HasRange (Ranged a) Source # | |
| HasRange a => HasRange (RecordDirectives' a) Source # | |
Defined in Agda.Syntax.Common Methods getRange :: RecordDirectives' a -> Range Source # | |
| HasRange a => HasRange (WithHiding a) Source # | |
Defined in Agda.Syntax.Common Methods getRange :: WithHiding a -> Range Source # | |
| HasRange a => HasRange (WithOrigin a) Source # | |
Defined in Agda.Syntax.Common Methods getRange :: WithOrigin a -> Range Source # | |
| HasRange a => HasRange (FieldAssignment' a) Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: FieldAssignment' a -> Range Source # | |
| HasRange e => HasRange (OpApp e) Source # | |
| IsExpr e => HasRange (ExprView e) Source # | |
| HasRange (DefInfo' t) Source # | |
| HasRange a => HasRange (PrintRange a) Source # | |
Defined in Agda.Syntax.Position Methods getRange :: PrintRange a -> Range Source # | |
| HasRange (TopLevelModuleName' Range) Source # | |
Defined in Agda.Syntax.Position | |
| HasRange a => HasRange (Closure a) Source # | |
| HasRange a => HasRange (List1 a) Source # | Precondition: The ranges of the list elements must point to the same file (or be empty). |
| HasRange a => HasRange (List2 a) Source # | |
| HasRange a => HasRange (Maybe a) Source # | |
| HasRange a => HasRange [a] Source # | Precondition: The ranges of the list elements must point to the same file (or be empty). |
Defined in Agda.Syntax.Position | |
| (HasRange a, HasRange b) => HasRange (ImportDirective' a b) Source # | |
Defined in Agda.Syntax.Common Methods getRange :: ImportDirective' a b -> Range Source # | |
| (HasRange a, HasRange b) => HasRange (ImportedName' a b) Source # | |
Defined in Agda.Syntax.Common Methods getRange :: ImportedName' a b -> Range Source # | |
| HasRange a => HasRange (Named name a) Source # | |
| (HasRange a, HasRange b) => HasRange (Renaming' a b) Source # | |
| (HasRange a, HasRange b) => HasRange (Using' a b) Source # | |
| HasRange a => HasRange (Dom' t a) Source # | |
| (HasRange a, HasRange b) => HasRange (Either a b) Source # | |
Defined in Agda.Syntax.Position | |
| (HasRange a, HasRange b) => HasRange (a, b) Source # | Precondition: The ranges of the tuple elements must point to the same file (or be empty). |
Defined in Agda.Syntax.Position | |
| (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). |
Defined in Agda.Syntax.Position | |
| (HasRange qn, HasRange nm, HasRange p, HasRange e) => HasRange (RewriteEqn' qn nm p e) Source # | |
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). |
Defined in Agda.Syntax.Position | |
| (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). |
Defined in Agda.Syntax.Position | |
| (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). |
Defined in Agda.Syntax.Position | |
| (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). |
Defined in Agda.Syntax.Position | |
class HasRange a => SetRange a where Source #
If it is also possible to set the range, this is the class.
Minimal complete definition
Nothing
Methods
Instances
| SetRange BindName Source # | |
| SetRange ModuleName Source # | |
Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> ModuleName -> ModuleName Source # | |
| SetRange Name Source # | |
| SetRange QName Source # | |
| SetRange Cohesion Source # | |
| SetRange NotationPart Source # | |
Defined in Agda.Syntax.Common Methods setRange :: Range -> NotationPart -> NotationPart Source # | |
| SetRange Q0Origin Source # | |
| SetRange Q1Origin Source # | |
| SetRange Quantity Source # | |
| SetRange QωOrigin Source # | |
| SetRange Relevance Source # | |
| SetRange Pattern Source # | |
| SetRange TypedBinding Source # | |
Defined in Agda.Syntax.Concrete Methods setRange :: Range -> TypedBinding -> TypedBinding Source # | |
| SetRange Attribute Source # | |
| SetRange Name Source # | |
| SetRange QName Source # | |
| SetRange ConPatInfo Source # | |
Defined in Agda.Syntax.Info Methods setRange :: Range -> ConPatInfo -> ConPatInfo Source # | |
| SetRange DeclInfo Source # | |
| SetRange ModuleInfo Source # | |
Defined in Agda.Syntax.Info Methods setRange :: Range -> ModuleInfo -> ModuleInfo Source # | |
| SetRange PatInfo Source # | |
| SetRange ConHead Source # | |
| SetRange Attr Source # | |
| SetRange Range Source # | |
| SetRange AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Methods setRange :: Range -> AbstractName -> AbstractName Source # | |
| SetRange RawTopLevelModuleName Source # | |
Defined in Agda.Syntax.TopLevelModuleName Methods setRange :: Range -> RawTopLevelModuleName -> RawTopLevelModuleName Source # | |
| SetRange MetaInfo Source # | |
| SetRange MetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods setRange :: Range -> MetaVariable -> MetaVariable Source # | |
| SetRange (Pattern' a) Source # | |
| SetRange a => SetRange (Arg a) Source # | |
| SetRange a => SetRange (WithHiding a) Source # | |
Defined in Agda.Syntax.Common Methods setRange :: Range -> WithHiding a -> WithHiding a Source # | |
| SetRange a => SetRange (WithOrigin a) Source # | |
Defined in Agda.Syntax.Common Methods setRange :: Range -> WithOrigin a -> WithOrigin a Source # | |
| SetRange (DefInfo' t) Source # | |
| SetRange a => SetRange (PrintRange a) Source # | |
Defined in Agda.Syntax.Position Methods setRange :: Range -> PrintRange a -> PrintRange a Source # | |
| SetRange (TopLevelModuleName' Range) Source # | |
Defined in Agda.Syntax.Position Methods setRange :: Range -> TopLevelModuleName' Range -> TopLevelModuleName' Range Source # | |
| SetRange a => SetRange (Maybe a) Source # | |
| SetRange a => SetRange [a] Source # | |
Defined in Agda.Syntax.Position | |
| SetRange a => SetRange (Named name a) Source # | |
class KillRange a where Source #
Killing the range of an object sets all range information to noRange.
Minimal complete definition
Nothing
Methods
killRange :: KillRangeT a Source #
default killRange :: forall (f :: Type -> Type) b. (Functor f, KillRange b, f b ~ a) => KillRangeT a Source #
Instances
| KillRange BindName Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange DataDefParams Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange Declaration Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange Expr Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange GeneralizeTelescope Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange LHS Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange LamBinding Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange LetBinding Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange ModuleApplication Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange ProblemEq Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange RHS Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange ScopeCopyInfo Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange SpineLHS Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange TypedBinding Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange TypedBindingInfo Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange WhereDeclarations Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange AmbiguousQName Source # | |
Defined in Agda.Syntax.Abstract.Name Methods | |
| KillRange ModuleName Source # | |
Defined in Agda.Syntax.Abstract.Name Methods | |
| KillRange Name Source # | |
Defined in Agda.Syntax.Abstract.Name Methods | |
| KillRange QName Source # | |
Defined in Agda.Syntax.Abstract.Name Methods | |
| KillRange Suffix Source # | |
Defined in Agda.Syntax.Abstract Methods | |
| KillRange BuiltinId Source # | |
Defined in Agda.Syntax.Builtin Methods | |
| KillRange PrimitiveId Source # | |
Defined in Agda.Syntax.Builtin Methods | |
| KillRange Access Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Annotation Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange ArgInfo Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Cohesion Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange ConOrigin Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange CoverageCheck Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Erased Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Fixity Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Fixity' Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Hiding Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange InteractionId Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange IsAbstract Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange IsInstance Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange IsMacro Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange IsOpaque Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Language Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Modality Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange NameId Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange NotationPart Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange OpaqueId Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Origin Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange OverlapMode Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange PositivityCheck Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange ProjOrigin Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Q0Origin Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Q1Origin Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Quantity Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange QωOrigin Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Relevance Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange UniverseCheck Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange Induction Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange KwRange Source # | |
Defined in Agda.Syntax.Common.KeywordRange Methods | |
| KillRange AsName Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange Binder Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange BoundName Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange Declaration Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange DoStmt Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange Expr Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange LHS Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange LamBinding Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange LamClause Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange ModuleApplication Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange ModuleAssignment Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange Pattern Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange Pragma Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange RHS Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange RecordDirective Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange TypedBinding Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange WhereClause Source # | |
Defined in Agda.Syntax.Concrete Methods | |
| KillRange Attribute Source # | |
Defined in Agda.Syntax.Concrete.Attribute Methods | |
| KillRange Name Source # | |
Defined in Agda.Syntax.Concrete.Name Methods | |
| KillRange QName Source # | |
Defined in Agda.Syntax.Concrete.Name Methods | |
| KillRange AppInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
| KillRange ConPatInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
| KillRange DeclInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
| KillRange ExprInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
| KillRange LHSInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
| KillRange LetInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
| KillRange MetaInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
| KillRange ModuleInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
| KillRange MutualInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
| KillRange PatInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
| KillRange Clause Source # | |
Defined in Agda.Syntax.Internal Methods | |
| KillRange ConHead Source # | |
Defined in Agda.Syntax.Internal Methods | |
| KillRange ConPatternInfo Source # | |
Defined in Agda.Syntax.Internal Methods | |
| KillRange DBPatVar Source # | |
Defined in Agda.Syntax.Internal Methods | |
| KillRange DataOrRecord Source # | |
Defined in Agda.Syntax.Internal Methods | |
| KillRange Level Source # | |
Defined in Agda.Syntax.Internal Methods | |
| KillRange PatOrigin Source # | |
Defined in Agda.Syntax.Internal Methods | |
| KillRange PatternInfo Source # | |
Defined in Agda.Syntax.Internal Methods | |
| KillRange PlusLevel Source # | |
Defined in Agda.Syntax.Internal Methods | |
| KillRange Sort Source # | |
Defined in Agda.Syntax.Internal Methods | |
| KillRange Substitution Source # | |
Defined in Agda.Syntax.Internal Methods | |
| KillRange Term Source # | |
Defined in Agda.Syntax.Internal Methods | |
| KillRange Literal Source # | |
Defined in Agda.Syntax.Literal Methods | |
| KillRange Range Source # | |
Defined in Agda.Syntax.Position Methods | |
| KillRange ScopeInfo Source # | |
Defined in Agda.Syntax.Scope.Base Methods | |
| KillRange RawTopLevelModuleName Source # | |
Defined in Agda.Syntax.TopLevelModuleName Methods | |
| KillRange Compiled Source # | |
Defined in Agda.Syntax.Treeless Methods | |
| KillRange CompiledClauses Source # | |
Defined in Agda.TypeChecking.CompiledClause Methods | |
| KillRange SplitTag Source # | |
Defined in Agda.TypeChecking.Coverage.SplitTree Methods | |
| KillRange BuiltinSort Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange CompKit Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange CompiledRepresentation Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange Definition Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange Definitions Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange Defn Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange DisplayForm Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange DisplayTerm Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange DoGeneralize Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange ExtLamInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange FunctionFlag Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange InstanceInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange InstanceTable Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange IsForced Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange MutualId Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange NLPSort Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange NLPType Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange NLPat Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange NumGeneralizableArgs Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange Polarity Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange ProjLams Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange Projection Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange ProjectionLikenessMissing Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange RewriteRule Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange RewriteRuleMap Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange Section Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange Sections Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange Signature Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange System Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange TermHead Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange Occurrence Source # | |
Defined in Agda.TypeChecking.Positivity.Occurrence Methods | |
| KillRange Permutation Source # | |
Defined in Agda.Syntax.Position Methods | |
| KillRange Void Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Void Source # | |
| KillRange Integer Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Integer Source # | |
| KillRange String Source # | Overlaps with |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT String Source # | |
| KillRange () Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT () Source # | |
| KillRange Bool Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Bool Source # | |
| KillRange Int Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Int Source # | |
| KillRange a => KillRange (Binder' a) Source # | |
Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Binder' a) Source # | |
| KillRange a => KillRange (Clause' a) Source # | |
Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Clause' a) Source # | |
| KillRange e => KillRange (LHSCore' e) Source # | |
Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (LHSCore' e) Source # | |
| KillRange e => KillRange (Pattern' e) Source # | |
Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Pattern' e) Source # | |
| KillRange a => KillRange (Arg a) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Arg a) Source # | |
| KillRange a => KillRange (HasEta' a) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (HasEta' a) Source # | |
| KillRange a => KillRange (MaybePlaceholder a) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (MaybePlaceholder a) Source # | |
| KillRange (Ranged a) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Ranged a) Source # | |
| KillRange a => KillRange (RecordDirectives' a) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (RecordDirectives' a) Source # | |
| KillRange m => KillRange (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (TerminationCheck m) Source # | |
| KillRange a => KillRange (WithHiding a) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (WithHiding a) Source # | |
| KillRange a => KillRange (WithOrigin a) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (WithOrigin a) Source # | |
| KillRange a => KillRange (FieldAssignment' a) Source # | |
Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (FieldAssignment' a) Source # | |
| KillRange e => KillRange (OpApp e) Source # | |
Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (OpApp e) Source # | |
| KillRange (TacticAttribute' a) Source # | |
Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (TacticAttribute' a) Source # | |
| KillRange x => KillRange (ThingWithFixity x) Source # | |
Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) Source # | |
| KillRange t => KillRange (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info Methods killRange :: KillRangeT (DefInfo' t) Source # | |
| KillRange a => KillRange (Abs a) Source # | |
Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Abs a) Source # | |
| KillRange a => KillRange (Blocked a) Source # | |
Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Blocked a) Source # | |
| KillRange a => KillRange (Pattern' a) Source # | |
Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Pattern' a) Source # | |
| KillRange a => KillRange (Tele a) Source # | |
Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Tele a) Source # | |
| KillRange a => KillRange (Type' a) Source # | |
Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Type' a) Source # | |
| KillRange a => KillRange (Elim' a) Source # | |
Defined in Agda.Syntax.Internal.Elim Methods killRange :: KillRangeT (Elim' a) Source # | |
| KillRange a => KillRange (PrintRange a) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (PrintRange a) Source # | |
| KillRange (TopLevelModuleName' Range) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (TopLevelModuleName' Range) Source # | |
| KillRange c => KillRange (Case c) Source # | |
Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (Case c) Source # | |
| KillRange c => KillRange (WithArity c) Source # | |
Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (WithArity c) Source # | |
| KillRange a => KillRange (SplitTree' a) Source # | |
Defined in Agda.TypeChecking.Coverage.SplitTree Methods killRange :: KillRangeT (SplitTree' a) Source # | |
| (KillRange a, Ord a) => KillRange (DiscrimTree a) Source # | |
Defined in Agda.TypeChecking.DiscrimTree.Types Methods killRange :: KillRangeT (DiscrimTree a) Source # | |
| KillRange a => KillRange (Closure a) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (Closure a) Source # | |
| KillRange c => KillRange (FunctionInverse' c) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (FunctionInverse' c) Source # | |
| KillRange a => KillRange (Open a) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (Open a) Source # | |
| KillRange a => KillRange (List1 a) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (List1 a) Source # | |
| KillRange a => KillRange (List2 a) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (List2 a) Source # | |
| KillRange a => KillRange (Drop a) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Drop a) Source # | |
| KillRange (SmallSet FunctionFlag) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| (Ord a, KillRange a) => KillRange (Set a) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Set a) Source # | |
| KillRange a => KillRange (Maybe a) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Maybe a) Source # | |
| KillRange a => KillRange (Maybe a) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Maybe a) Source # | |
| KillRange a => KillRange [a] Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT [a] Source # | |
| (KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportDirective' a b) Source # | |
| (KillRange a, KillRange b) => KillRange (ImportedName' a b) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportedName' a b) Source # | |
| (KillRange name, KillRange a) => KillRange (Named name a) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Named name a) Source # | |
| (KillRange a, KillRange b) => KillRange (Renaming' a b) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Renaming' a b) Source # | |
| (KillRange a, KillRange b) => KillRange (Using' a b) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Using' a b) Source # | |
| (KillRange t, KillRange a) => KillRange (Dom' t a) Source # | |
Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Dom' t a) Source # | |
| KillRange a => KillRange (Map k a) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Map k a) Source # | |
| (KillRange a, KillRange b) => KillRange (Either a b) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Either a b) Source # | |
| (KillRange a, KillRange b) => KillRange (a, b) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (a, b) Source # | |
| (KillRange a, KillRange b, KillRange c) => KillRange (a, b, c) Source # | |
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 # | |
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 # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (a, b, c, d) Source # | |
type KillRangeT a = a -> a Source #
killRangeMap :: (KillRange k, KillRange v) => KillRangeT (Map k v) Source #
Remove ranges in keys and values of a map.
class KILLRANGE t (b :: Bool) where Source #
Methods
killRangeN :: t -> t Source #
Instances
| IsBase t ~ 'True => KILLRANGE t 'True Source # | |
Defined in Agda.Syntax.Position Methods killRangeN :: t -> t Source # | |
| KILLRANGE t (IsBase t) => KILLRANGE (a -> t) 'False Source # | |
Defined in Agda.Syntax.Position Methods killRangeN :: (a -> t) -> a -> t Source # | |
withRangeOf :: (SetRange t, HasRange u) => t -> u -> t Source #
x `withRangeOf` y sets the range of x to the range of y.
fuseRange :: (HasRange u, HasRange t) => u -> t -> Range Source #
Precondition: The ranges must point to the same file (or be empty).
fuseRanges :: Ord a => Range' a -> Range' a -> Range' a Source #
fuseRanges r r' unions the ranges r and r'.
Meaning it finds the least range r0 that covers r and r'.
Precondition: The ranges must point to the same file (or be empty).
beginningOf :: Range -> Range Source #
beginningOf r is an empty range (a single, empty interval)
positioned at the beginning of r. If r does not have a
beginning, then noRange is returned.
beginningOfFile :: 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.