| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Mikan.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' {
- srcFile :: !a
- posPos :: !Word32
- posLineCol :: !Word64
- pattern Pn :: a -> Word32 -> Word32 -> Word32 -> Position' a
- posLine :: Position' a -> Word32
- posCol :: Position' a -> Word32
- type SrcFile = Maybe RangeFile
- data RangeFile = RangeFile {}
- mkRangeFile :: AbsolutePath -> Maybe (TopLevelModuleName' Range) -> RangeFile
- positionInvariant :: Position' a -> Bool
- startPos :: Maybe RangeFile -> Position
- startPos' :: a -> Position' a
- movePos :: Position' a -> Char -> Position' a
- movePosByString :: Position' a -> Text -> Position' a
- backupPos :: Position' a -> Position' a
- type Interval = Interval' SrcFile
- type IntervalWithoutFile = Interval' ()
- data IntervalWithoutFile'
- pattern PackIWF :: IntervalWithoutFile -> IntervalWithoutFile'
- unpackIWF :: IntervalWithoutFile' -> IntervalWithoutFile
- data Interval' a = Interval a !PositionWithoutFile !PositionWithoutFile
- intervalInvariant :: Ord a => Interval' a -> Bool
- iStart :: Interval' a -> Position' a
- iEnd :: Interval' a -> Position' a
- posToInterval :: a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
- getIntervalFile :: Interval' a -> a
- iLength :: Interval' a -> Word32
- fuseIntervals :: IntervalWithoutFile -> IntervalWithoutFile -> IntervalWithoutFile
- type Range = Range' SrcFile
- type RangeWithoutFile = Range' ()
- data Range' a
- = NoRange
- | Range !a (Seq IntervalWithoutFile')
- rangeInvariant :: Range' a -> Bool
- consecutiveAndSeparated :: Ord a => [Interval' a] -> Bool
- intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a
- intervalToRange :: a -> IntervalWithoutFile -> Range' a
- rangeFromAbsolutePath :: AbsolutePath -> Range
- rangeIntervals :: Range' a -> [IntervalWithoutFile]
- rangeFile :: Range -> SrcFile
- rangeModule' :: Range -> Maybe (Maybe (TopLevelModuleName' Range))
- rangeModule :: Range -> Maybe (TopLevelModuleName' Range)
- rightMargin :: Range -> Range
- noRange :: Range' a
- posToRange :: Position' a -> Position' b -> 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 :: Range' a -> Range' a
- newtype PrintRange a = PrintRange a
- class HasRange a where
- class HasRangeWithoutFile a where
- getRangeWithoutFile :: a -> RangeWithoutFile
- 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 :: Range' a -> Range' a -> Range' a
- beginningOf :: Range -> Range
- beginningOfFile :: BeginningOfFile a => a -> Range
- interleaveRanges :: HasRangeWithoutFile 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' | |
Fields
| |
Instances
Constructors
| RangeFile | |
Fields
| |
Instances
| EncodeTCM Range Source # | |||||
| Pretty RangeFile Source # | |||||
| Pretty TopLevelModuleName Source # | |||||
Defined in Mikan.Syntax.TopLevelModuleName Methods pretty :: TopLevelModuleName -> Doc Source # prettyPrec :: Int -> TopLevelModuleName -> Doc Source # prettyList :: [TopLevelModuleName] -> Doc Source # | |||||
| HasRange Interval Source # | |||||
| HasRange Range Source # | |||||
| HasRangeWithoutFile Range Source # | |||||
Defined in Mikan.Syntax.Position Methods | |||||
| KillRange Range Source # | |||||
Defined in Mikan.Syntax.Position Methods | |||||
| SetRange Range Source # | |||||
| FreshName Range Source # | |||||
Defined in Mikan.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => Range -> m Name Source # | |||||
| PrettyTCM Range Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| PrettyTCM TopLevelModuleName Source # | |||||
Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TopLevelModuleName -> m Doc Source # | |||||
| EmbPrj Range Source # | Ranges are always deserialised as | ||||
| EmbPrj RangeFile Source # | |||||
| EmbPrj TopLevelModuleName Source # | |||||
| Subst Range Source # | |||||
Defined in Mikan.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source # | |||||
| Null RangeFile Source # | |||||
| Sized TopLevelModuleName Source # | |||||
Defined in Mikan.Syntax.TopLevelModuleName | |||||
| ToJSON Range Source # | |||||
| NFData Interval Source # | |||||
Defined in Mikan.Syntax.Position | |||||
| NFData Position Source # | |||||
Defined in Mikan.Syntax.Position | |||||
| NFData RangeFile Source # | |||||
Defined in Mikan.Syntax.Position | |||||
| Generic RangeFile Source # | |||||
Defined in Mikan.Syntax.Position Associated Types
| |||||
| Read RangeFile Source # | This instance fills in the | ||||
| Show RangeFile Source # | |||||
| Eq RangeFile Source # | Only the | ||||
| Ord RangeFile Source # | Only the | ||||
| Hashable RangeFile Source # | |||||
Defined in Mikan.Syntax.Position | |||||
| LensClosure MetaInfo Range Source # | |||||
Defined in Mikan.TypeChecking.Monad.Base | |||||
| LensClosure MetaVariable Range Source # | |||||
Defined in Mikan.TypeChecking.Monad.Base Methods | |||||
| HasRange (TopLevelModuleName' Range) Source # | |||||
Defined in Mikan.Syntax.Position | |||||
| KillRange (TopLevelModuleName' Range) Source # | |||||
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (TopLevelModuleName' Range) Source # | |||||
| SetRange (TopLevelModuleName' Range) Source # | |||||
Defined in Mikan.Syntax.Position Methods setRange :: Range -> TopLevelModuleName' Range -> TopLevelModuleName' Range Source # | |||||
| FreshName (Range, ShortText) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => (Range, ShortText) -> m Name Source # | |||||
| type SubstArg Range Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
| type Rep RangeFile Source # | |||||
Defined in Mikan.Syntax.Position type Rep RangeFile = D1 ('MetaData "RangeFile" "Mikan.Syntax.Position" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "RangeFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "rangeFilePath") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 AbsolutePath) :*: S1 ('MetaSel ('Just "rangeFileName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (TopLevelModuleName' Range))))) | |||||
mkRangeFile :: AbsolutePath -> Maybe (TopLevelModuleName' Range) -> RangeFile Source #
A smart constructor for RangeFile.
positionInvariant :: Position' a -> Bool Source #
startPos :: Maybe RangeFile -> Position Source #
The first position in a file: position 1, line 1, column 1.
movePos :: Position' a -> Char -> Position' a Source #
Advance the position by one character.
A newline character ('n') moves the position to the first
character in the next line. Any other character moves the
position to the next column.
movePosByString :: Position' a -> Text -> 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 #
data IntervalWithoutFile' Source #
Tolerably efficient representation of IntervalWithoutFile
Instances
| NFData IntervalWithoutFile' Source # | |
Defined in Mikan.Syntax.Position Methods rnf :: IntervalWithoutFile' -> () # | |
| Show IntervalWithoutFile' Source # | |
Defined in Mikan.Syntax.Position Methods showsPrec :: Int -> IntervalWithoutFile' -> ShowS # show :: IntervalWithoutFile' -> String # showList :: [IntervalWithoutFile'] -> ShowS # | |
| Eq IntervalWithoutFile' Source # | |
Defined in Mikan.Syntax.Position Methods (==) :: IntervalWithoutFile' -> IntervalWithoutFile' -> Bool # (/=) :: IntervalWithoutFile' -> IntervalWithoutFile' -> Bool # | |
| Ord IntervalWithoutFile' Source # | |
Defined in Mikan.Syntax.Position Methods compare :: IntervalWithoutFile' -> IntervalWithoutFile' -> Ordering # (<) :: IntervalWithoutFile' -> IntervalWithoutFile' -> Bool # (<=) :: IntervalWithoutFile' -> IntervalWithoutFile' -> Bool # (>) :: IntervalWithoutFile' -> IntervalWithoutFile' -> Bool # (>=) :: IntervalWithoutFile' -> IntervalWithoutFile' -> Bool # max :: IntervalWithoutFile' -> IntervalWithoutFile' -> IntervalWithoutFile' # min :: IntervalWithoutFile' -> IntervalWithoutFile' -> IntervalWithoutFile' # | |
| Hashable IntervalWithoutFile' Source # | |
Defined in Mikan.Syntax.Position | |
pattern PackIWF :: IntervalWithoutFile -> IntervalWithoutFile' Source #
An interval. The iEnd position is not included in the interval.
Note the invariant which intervals have to satisfy: intervalInvariant.
Constructors
| Interval a !PositionWithoutFile !PositionWithoutFile |
Instances
| HasRange Interval Source # | |||||
| HasRangeWithoutFile IntervalWithoutFile Source # | |||||
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: IntervalWithoutFile -> RangeWithoutFile Source # | |||||
| NFData Interval Source # | |||||
Defined in Mikan.Syntax.Position | |||||
| NFData IntervalWithoutFile Source # | |||||
Defined in Mikan.Syntax.Position Methods rnf :: IntervalWithoutFile -> () # | |||||
| Functor Interval' Source # | |||||
| Foldable Interval' Source # | |||||
Defined in Mikan.Syntax.Position Methods fold :: Monoid m => Interval' m -> m # foldMap :: Monoid m => (a -> m) -> Interval' a -> m # foldMap' :: Monoid m => (a -> m) -> Interval' a -> m # foldr :: (a -> b -> b) -> b -> Interval' a -> b # foldr' :: (a -> b -> b) -> b -> Interval' a -> b # foldl :: (b -> a -> b) -> b -> Interval' a -> b # foldl' :: (b -> a -> b) -> b -> Interval' a -> b # foldr1 :: (a -> a -> a) -> Interval' a -> a # foldl1 :: (a -> a -> a) -> Interval' a -> a # toList :: Interval' a -> [a] # length :: Interval' a -> Int # elem :: Eq a => a -> Interval' a -> Bool # maximum :: Ord a => Interval' a -> a # minimum :: Ord a => Interval' a -> a # | |||||
| Traversable Interval' Source # | |||||
Defined in Mikan.Syntax.Position | |||||
| Pretty a => Pretty (Interval' a) Source # | |||||
| EmbPrj a => EmbPrj (Interval' a) Source # | |||||
| Generic (Interval' a) Source # | |||||
Defined in Mikan.Syntax.Position Associated Types
| |||||
| Read a => Read (Interval' a) Source # | |||||
| Show a => Show (Interval' a) Source # | |||||
| Eq a => Eq (Interval' a) Source # | |||||
| Ord a => Ord (Interval' a) Source # | |||||
Defined in Mikan.Syntax.Position | |||||
| Hashable a => Hashable (Interval' a) Source # | |||||
Defined in Mikan.Syntax.Position | |||||
| type Rep (Interval' a) Source # | |||||
Defined in Mikan.Syntax.Position type Rep (Interval' a) = D1 ('MetaData "Interval'" "Mikan.Syntax.Position" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "Interval" 'PrefixI 'True) (S1 ('MetaSel ('Just "getIntervalFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Just "iStart'") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PositionWithoutFile) :*: S1 ('MetaSel ('Just "iEnd'") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PositionWithoutFile)))) | |||||
posToInterval :: a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a Source #
Converts a file name and two positions to an interval. Sort the positions ascendingly.
getIntervalFile :: Interval' a -> a Source #
fuseIntervals :: IntervalWithoutFile -> IntervalWithoutFile -> IntervalWithoutFile Source #
Finds the least interval which covers the arguments.
Ranges
type RangeWithoutFile = Range' () Source #
A range is a file name, plus a sequence of intervals, assumed to point to the given file. The intervals should be consecutive and separated.
Note the invariant which ranges have to satisfy: rangeInvariant.
Constructors
| NoRange | |
| Range !a (Seq IntervalWithoutFile') |
Instances
| EncodeTCM Range Source # | |||||
| Pretty TopLevelModuleName Source # | |||||
Defined in Mikan.Syntax.TopLevelModuleName Methods pretty :: TopLevelModuleName -> Doc Source # prettyPrec :: Int -> TopLevelModuleName -> Doc Source # prettyList :: [TopLevelModuleName] -> Doc Source # | |||||
| HasRange Range Source # | |||||
| HasRangeWithoutFile Range Source # | |||||
Defined in Mikan.Syntax.Position Methods | |||||
| HasRangeWithoutFile RangeWithoutFile Source # | |||||
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: RangeWithoutFile -> RangeWithoutFile Source # | |||||
| KillRange Range Source # | |||||
Defined in Mikan.Syntax.Position Methods | |||||
| SetRange Range Source # | |||||
| FreshName Range Source # | |||||
Defined in Mikan.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => Range -> m Name Source # | |||||
| PrettyTCM Range Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| PrettyTCM TopLevelModuleName Source # | |||||
Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TopLevelModuleName -> m Doc Source # | |||||
| EmbPrj Range Source # | Ranges are always deserialised as | ||||
| EmbPrj TopLevelModuleName Source # | |||||
| Subst Range Source # | |||||
Defined in Mikan.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source # | |||||
| Sized TopLevelModuleName Source # | |||||
Defined in Mikan.Syntax.TopLevelModuleName | |||||
| ToJSON Range Source # | |||||
| Functor Range' Source # | |||||
| Foldable Range' Source # | |||||
Defined in Mikan.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 # minimum :: Ord a => Range' a -> a # | |||||
| Traversable Range' Source # | |||||
| LensClosure MetaInfo Range Source # | |||||
Defined in Mikan.TypeChecking.Monad.Base | |||||
| LensClosure MetaVariable Range Source # | |||||
Defined in Mikan.TypeChecking.Monad.Base Methods | |||||
| Pretty a => Pretty (Range' a) Source # | |||||
| HasRange (TopLevelModuleName' Range) Source # | |||||
Defined in Mikan.Syntax.Position | |||||
| KillRange (TopLevelModuleName' Range) Source # | |||||
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (TopLevelModuleName' Range) Source # | |||||
| SetRange (TopLevelModuleName' Range) Source # | |||||
Defined in Mikan.Syntax.Position Methods setRange :: Range -> TopLevelModuleName' Range -> TopLevelModuleName' Range Source # | |||||
| Null (Range' a) Source # | |||||
| NFData a => NFData (Range' a) Source # | |||||
Defined in Mikan.Syntax.Position | |||||
| Eq a => Monoid (Range' a) Source # | |||||
| Eq a => Semigroup (Range' a) Source # | |||||
| Generic (Range' a) Source # | |||||
Defined in Mikan.Syntax.Position Associated Types
| |||||
| Read a => Read (Range' a) Source # | Note that the grammar implemented by this instance does not necessarily match the current representation of ranges. | ||||
| Show a => Show (Range' a) Source # | |||||
| Eq a => Eq (Range' a) Source # | |||||
| Ord a => Ord (Range' a) Source # | |||||
Defined in Mikan.Syntax.Position | |||||
| Hashable a => Hashable (Range' a) Source # | |||||
Defined in Mikan.Syntax.Position | |||||
| FreshName (Range, ShortText) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => (Range, ShortText) -> m Name Source # | |||||
| type SubstArg Range Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
| type Rep (Range' a) Source # | |||||
Defined in Mikan.Syntax.Position type Rep (Range' a) = D1 ('MetaData "Range'" "Mikan.Syntax.Position" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" '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 :: Range' a -> Bool Source #
Range invariant.
consecutiveAndSeparated :: Ord a => [Interval' a] -> Bool Source #
Are the intervals consecutive and separated, do they all point to the same file, and do they satisfy the interval invariant?
intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a Source #
Turns a file name plus a list of intervals into a range.
Precondition: consecutiveAndSeparated.
intervalToRange :: a -> IntervalWithoutFile -> Range' a Source #
Converts a file name and an interval to a range.
rangeFromAbsolutePath :: AbsolutePath -> Range Source #
Range pointing to the first position in the given file.
rangeIntervals :: Range' a -> [IntervalWithoutFile] Source #
The intervals that make up the range. The intervals are
consecutive and separated (consecutiveAndSeparated).
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' b -> 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 :: 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 Mikan.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 Mikan.Syntax.Position Methods getRange :: PrintRange a -> Range Source # | |
| KillRange a => KillRange (PrintRange a) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (PrintRange a) Source # | |
| SetRange a => SetRange (PrintRange a) Source # | |
Defined in Mikan.Syntax.Position Methods setRange :: Range -> PrintRange a -> PrintRange a Source # | |
| Eq a => Eq (PrintRange a) Source # | |
Defined in Mikan.Syntax.Position | |
| Ord a => Ord (PrintRange a) Source # | |
Defined in Mikan.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 BindName Source # | |
| HasRange Declaration Source # | |
Defined in Mikan.Syntax.Abstract Methods getRange :: Declaration -> Range Source # | |
| HasRange Expr Source # | |
| HasRange LHS Source # | |
| HasRange LamBinding Source # | |
Defined in Mikan.Syntax.Abstract Methods getRange :: LamBinding -> Range Source # | |
| HasRange LetBinding Source # | |
Defined in Mikan.Syntax.Abstract Methods getRange :: LetBinding -> Range Source # | |
| HasRange RHS Source # | |
| HasRange SpineLHS Source # | |
| HasRange TypedBinding Source # | |
Defined in Mikan.Syntax.Abstract Methods getRange :: TypedBinding -> Range Source # | |
| HasRange WhereDeclarations Source # | |
Defined in Mikan.Syntax.Abstract Methods getRange :: WhereDeclarations -> Range Source # | |
| HasRange AbstractName Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods getRange :: AbstractName -> Range Source # | |
| HasRange AmbQNameEntry Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods getRange :: AmbQNameEntry -> Range Source # | |
| HasRange AmbiguousQName Source # | The range of an |
Defined in Mikan.Syntax.Abstract.Name Methods getRange :: AmbiguousQName -> Range Source # | |
| HasRange ConHead Source # | |
| HasRange ModuleName Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods getRange :: ModuleName -> Range Source # | |
| HasRange Name Source # | |
| HasRange QName Source # | |
| HasRange Access Source # | |
| HasRange ArgInfo Source # | |
| HasRange Fixity Source # | |
| HasRange Fixity' Source # | |
| HasRange Hiding Source # | |
| HasRange IsInstance Source # | |
Defined in Mikan.Syntax.Common Methods getRange :: IsInstance -> Range Source # | |
| HasRange IsMacro Source # | |
| HasRange NotationPart Source # | |
Defined in Mikan.Syntax.Common Methods getRange :: NotationPart -> Range Source # | |
| HasRange Origin Source # | |
| HasRange PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common Methods getRange :: PatternOrCopattern -> Range Source # | |
| HasRange Induction Source # | |
| HasRange KwRange Source # | |
| HasRange AsName Source # | |
| HasRange Binder Source # | |
| HasRange BoundName Source # | |
| HasRange Declaration Source # | |
Defined in Mikan.Syntax.Concrete Methods getRange :: Declaration -> Range Source # | |
| HasRange DoStmt Source # | |
| HasRange Expr Source # | |
| HasRange LHS Source # | |
| HasRange LHSCore Source # | |
| HasRange LamBinding Source # | |
Defined in Mikan.Syntax.Concrete Methods getRange :: LamBinding -> Range Source # | |
| HasRange LamClause Source # | |
| HasRange ModuleApplication Source # | |
Defined in Mikan.Syntax.Concrete Methods getRange :: ModuleApplication -> Range Source # | |
| HasRange ModuleAssignment Source # | |
Defined in Mikan.Syntax.Concrete Methods getRange :: ModuleAssignment -> Range Source # | |
| HasRange OpenShortHand Source # | |
Defined in Mikan.Syntax.Concrete Methods getRange :: OpenShortHand -> Range Source # | |
| HasRange Pattern Source # | |
| HasRange Pragma Source # | |
| HasRange RHS Source # | |
| HasRange RecordDirective Source # | |
Defined in Mikan.Syntax.Concrete Methods getRange :: RecordDirective -> Range Source # | |
| HasRange TypedBinding Source # | |
Defined in Mikan.Syntax.Concrete Methods getRange :: TypedBinding -> Range Source # | |
| HasRange WhereClause Source # | |
Defined in Mikan.Syntax.Concrete Methods getRange :: WhereClause -> Range Source # | |
| HasRange Attr Source # | |
| HasRange Attribute Source # | |
| HasRange DeclarationException Source # | |
Defined in Mikan.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationException -> Range Source # | |
| HasRange DeclarationException' Source # | |
Defined in Mikan.Syntax.Concrete.Definitions.Errors Methods | |
| HasRange DeclarationWarning Source # | |
Defined in Mikan.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationWarning -> Range Source # | |
| HasRange DeclarationWarning' Source # | |
Defined in Mikan.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationWarning' -> Range Source # | |
| HasRange InterleavedDecl Source # | |
Defined in Mikan.Syntax.Concrete.Definitions.Types Methods getRange :: InterleavedDecl -> Range Source # | |
| HasRange NiceDeclaration Source # | |
Defined in Mikan.Syntax.Concrete.Definitions.Types Methods getRange :: NiceDeclaration -> Range Source # | |
| HasRange Name Source # | |
| HasRange QName Source # | |
| HasRange AppInfo Source # | |
| HasRange ConPatInfo Source # | |
Defined in Mikan.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 Mikan.Syntax.Info Methods getRange :: ModuleInfo -> Range Source # | |
| HasRange MutualInfo Source # | |
Defined in Mikan.Syntax.Info Methods getRange :: MutualInfo -> Range Source # | |
| HasRange PatInfo Source # | |
| HasRange Clause Source # | |
| HasRange ParseError Source # | |
Defined in Mikan.Syntax.Parser.Monad Methods getRange :: ParseError -> Range Source # | |
| HasRange ParseWarning Source # | |
Defined in Mikan.Syntax.Parser.Monad Methods getRange :: ParseWarning -> Range Source # | |
| HasRange QualifiedToken Source # | |
Defined in Mikan.Syntax.Parser.Tokens Methods getRange :: QualifiedToken -> Range Source # | |
| HasRange Token Source # | |
| HasRange Interval Source # | |
| HasRange Range Source # | |
| HasRange RawTopLevelModuleName Source # | |
Defined in Mikan.Syntax.TopLevelModuleName Methods | |
| HasRange DeferredError Source # | |
Defined in Mikan.TypeChecking.Errors.Deferred Methods getRange :: DeferredError -> Range Source # | |
| HasRange Call Source # | |
| HasRange CallInfo Source # | |
| HasRange CompilerPragma Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods getRange :: CompilerPragma -> Range Source # | |
| HasRange Constraint Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods getRange :: Constraint -> Range Source # | |
| HasRange MetaInfo Source # | |
| HasRange MetaVariable Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods getRange :: MetaVariable -> Range Source # | |
| HasRange ProblemConstraint Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods getRange :: ProblemConstraint -> Range Source # | |
| HasRange TCErr Source # | |
| HasRange UnsolvedWarning Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods getRange :: UnsolvedWarning -> Range Source # | |
| HasRange () Source # | |
Defined in Mikan.Syntax.Position | |
| HasRange Bool Source # | |
| 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 Mikan.Syntax.Common Methods getRange :: MaybePlaceholder a -> Range Source # | |
| HasRange (Ranged a) Source # | |
| HasRange a => HasRange (RecordDirectives' a) Source # | |
Defined in Mikan.Syntax.Common Methods getRange :: RecordDirectives' a -> Range Source # | |
| HasRange a => HasRange (WithHiding a) Source # | |
Defined in Mikan.Syntax.Common Methods getRange :: WithHiding a -> Range Source # | |
| HasRange a => HasRange (WithOrigin a) Source # | |
Defined in Mikan.Syntax.Common Methods getRange :: WithOrigin a -> Range Source # | |
| HasRange a => HasRange (FieldAssignment' a) Source # | |
Defined in Mikan.Syntax.Concrete Methods getRange :: FieldAssignment' a -> Range Source # | |
| HasRange e => HasRange (OpApp e) Source # | |
| HasRange (TacticAttribute' a) Source # | |
Defined in Mikan.Syntax.Concrete Methods getRange :: TacticAttribute' a -> Range Source # | |
| IsExpr e => HasRange (ExprView e) Source # | |
| HasRange (DefInfo' t) Source # | |
| HasRange a => HasRange (PrintRange a) Source # | |
Defined in Mikan.Syntax.Position Methods getRange :: PrintRange a -> Range Source # | |
| HasRange (TopLevelModuleName' Range) Source # | |
Defined in Mikan.Syntax.Position | |
| HasRange a => HasRange (Closure a) Source # | |
| HasRange (TCWarning' a) Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods getRange :: TCWarning' a -> Range Source # | |
| HasRange a => HasRange (List1 a) Source # | Precondition: The ranges of the list elements must point to the same file (or be empty). |
| HasRange a => HasRange (List2 a) Source # | |
| HasRange a => HasRange (Set1 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 Mikan.Syntax.Position | |
| HasRange (ImportDirective' a b) Source # | |
Defined in Mikan.Syntax.Common Methods getRange :: ImportDirective' a b -> Range Source # | |
| (HasRange a, HasRange b) => HasRange (ImportedName' a b) Source # | |
Defined in Mikan.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 # | |
| (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 Mikan.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 Mikan.Syntax.Position | |
| (HasRange qn, HasRange p, HasRange e) => HasRange (RewriteEqn' qn nm p e) Source # | |
Defined in Mikan.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 Mikan.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 Mikan.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 Mikan.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 Mikan.Syntax.Position | |
class HasRangeWithoutFile a where Source #
Things that have a RangeWithoutFile are instances of this class.
Minimal complete definition
Nothing
Methods
getRangeWithoutFile :: a -> RangeWithoutFile Source #
default getRangeWithoutFile :: forall (t :: Type -> Type) b. (Foldable t, HasRangeWithoutFile b, t b ~ a) => a -> RangeWithoutFile Source #
Instances
| HasRangeWithoutFile Layer Source # | |
Defined in Mikan.Syntax.Parser.Literate Methods | |
| HasRangeWithoutFile Token Source # | |
Defined in Mikan.Syntax.Parser.Tokens Methods | |
| HasRangeWithoutFile IntervalWithoutFile Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: IntervalWithoutFile -> RangeWithoutFile Source # | |
| HasRangeWithoutFile Range Source # | |
Defined in Mikan.Syntax.Position Methods | |
| HasRangeWithoutFile RangeWithoutFile Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: RangeWithoutFile -> RangeWithoutFile Source # | |
| HasRangeWithoutFile () Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: () -> RangeWithoutFile Source # | |
| HasRangeWithoutFile Bool Source # | |
Defined in Mikan.Syntax.Position Methods | |
| HasRangeWithoutFile a => HasRangeWithoutFile (List1 a) Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: List1 a -> RangeWithoutFile Source # | |
| HasRangeWithoutFile a => HasRangeWithoutFile (List2 a) Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: List2 a -> RangeWithoutFile Source # | |
| HasRangeWithoutFile a => HasRangeWithoutFile (Set1 a) Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: Set1 a -> RangeWithoutFile Source # | |
| HasRangeWithoutFile a => HasRangeWithoutFile (Maybe a) Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: Maybe a -> RangeWithoutFile Source # | |
| HasRangeWithoutFile a => HasRangeWithoutFile [a] Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: [a] -> RangeWithoutFile Source # | |
| (HasRangeWithoutFile a, HasRangeWithoutFile b) => HasRangeWithoutFile (Either a b) Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: Either a b -> RangeWithoutFile Source # | |
| (HasRangeWithoutFile a, HasRangeWithoutFile b) => HasRangeWithoutFile (a, b) Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: (a, b) -> RangeWithoutFile Source # | |
| (HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c) => HasRangeWithoutFile (a, b, c) Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: (a, b, c) -> RangeWithoutFile Source # | |
| (HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d) => HasRangeWithoutFile (a, b, c, d) Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: (a, b, c, d) -> RangeWithoutFile Source # | |
| (HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d, HasRangeWithoutFile e) => HasRangeWithoutFile (a, b, c, d, e) Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: (a, b, c, d, e) -> RangeWithoutFile Source # | |
| (HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d, HasRangeWithoutFile e, HasRangeWithoutFile f) => HasRangeWithoutFile (a, b, c, d, e, f) Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: (a, b, c, d, e, f) -> RangeWithoutFile Source # | |
| (HasRangeWithoutFile a, HasRangeWithoutFile b, HasRangeWithoutFile c, HasRangeWithoutFile d, HasRangeWithoutFile e, HasRangeWithoutFile f, HasRangeWithoutFile g) => HasRangeWithoutFile (a, b, c, d, e, f, g) Source # | |
Defined in Mikan.Syntax.Position Methods getRangeWithoutFile :: (a, b, c, d, e, f, g) -> RangeWithoutFile Source # | |
class HasRange a => SetRange a where Source #
If it is also possible to set the range, this is the class.
Minimal complete definition
Nothing
Methods
Instances
| SetRange BindName Source # | |
| SetRange AbstractName Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods setRange :: Range -> AbstractName -> AbstractName Source # | |
| SetRange ConHead Source # | |
| SetRange ModuleName Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods setRange :: Range -> ModuleName -> ModuleName Source # | |
| SetRange Name Source # | |
| SetRange QName Source # | |
| SetRange NotationPart Source # | |
Defined in Mikan.Syntax.Common Methods setRange :: Range -> NotationPart -> NotationPart Source # | |
| SetRange Pattern Source # | |
| SetRange TypedBinding Source # | |
Defined in Mikan.Syntax.Concrete Methods setRange :: Range -> TypedBinding -> TypedBinding Source # | |
| SetRange Attr Source # | |
| SetRange Attribute Source # | |
| SetRange Name Source # | |
| SetRange QName Source # | |
| SetRange ConPatInfo Source # | |
Defined in Mikan.Syntax.Info Methods setRange :: Range -> ConPatInfo -> ConPatInfo Source # | |
| SetRange DeclInfo Source # | |
| SetRange ModuleInfo Source # | |
Defined in Mikan.Syntax.Info Methods setRange :: Range -> ModuleInfo -> ModuleInfo Source # | |
| SetRange PatInfo Source # | |
| SetRange Range Source # | |
| SetRange RawTopLevelModuleName Source # | |
Defined in Mikan.Syntax.TopLevelModuleName Methods setRange :: Range -> RawTopLevelModuleName -> RawTopLevelModuleName Source # | |
| SetRange MetaInfo Source # | |
| SetRange MetaVariable Source # | |
Defined in Mikan.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 Mikan.Syntax.Common Methods setRange :: Range -> WithHiding a -> WithHiding a Source # | |
| SetRange a => SetRange (WithOrigin a) Source # | |
Defined in Mikan.Syntax.Common Methods setRange :: Range -> WithOrigin a -> WithOrigin a Source # | |
| SetRange (DefInfo' t) Source # | |
| SetRange a => SetRange (PrintRange a) Source # | |
Defined in Mikan.Syntax.Position Methods setRange :: Range -> PrintRange a -> PrintRange a Source # | |
| SetRange (TopLevelModuleName' Range) Source # | |
Defined in Mikan.Syntax.Position Methods setRange :: Range -> TopLevelModuleName' Range -> TopLevelModuleName' Range Source # | |
| SetRange a => SetRange (Maybe a) Source # | |
| SetRange a => SetRange [a] Source # | |
Defined in Mikan.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 #
Instances
| KillRange BindName Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange DataDefParams Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange Declaration Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange Expr Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange GeneralizeTelescope Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange LHS Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange LamBinding Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange LetBinding Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange ModuleApplication Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange PatternSynDefn Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange ProblemEq Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange RHS Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange RecordConName Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange ScopeCopyInfo Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange SpineLHS Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange TypedBinding Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange TypedBindingInfo Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange WhereDeclarations Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange AbstractName Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods | |
| KillRange AmbQNameEntry Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods | |
| KillRange AmbiguousQName Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods | |
| KillRange ConHead Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods | |
| KillRange KindOfName Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods | |
| KillRange ModuleName Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods | |
| KillRange Name Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods | |
| KillRange NameMetadata Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods | |
| KillRange QName Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods | |
| KillRange Suffix Source # | |
Defined in Mikan.Syntax.Abstract Methods | |
| KillRange WhyInScope Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods | |
| KillRange BuiltinId Source # | |
Defined in Mikan.Syntax.Builtin Methods | |
| KillRange PrimitiveId Source # | |
Defined in Mikan.Syntax.Builtin Methods | |
| KillRange Access Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange ArgInfo Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange BinderNameOrigin Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange Catchall Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange ConOrigin Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange CoverageCheck Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange DataOrRecord Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange ExpandedEllipsis Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange Fixity Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange Fixity' Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange FreeVariables Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange Hiding Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange InteractionId Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange IsAbstract Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange IsInstance Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange IsMacro Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange IsOpaque Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange NameId Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange NotationPart Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange OpaqueId Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange Origin Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange OverlapMode Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange PositivityCheck Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange ProjOrigin Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange UniverseCheck Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange Induction Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange KwRange Source # | |
Defined in Mikan.Syntax.Common.KeywordRange Methods | |
| KillRange AsName Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange Binder Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange BoundName Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange Declaration Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange DoStmt Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange Expr Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange LHS Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange LamBinding Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange LamClause Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange ModuleApplication Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange ModuleAssignment Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange OpenShortHand Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange Pattern Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange Pragma Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange RHS Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange RecordDirective Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange TypedBinding Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange WhereClause Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange Attr Source # | |
Defined in Mikan.Syntax.Concrete.Attribute Methods | |
| KillRange Attribute Source # | |
Defined in Mikan.Syntax.Concrete.Attribute Methods | |
| KillRange Name Source # | |
Defined in Mikan.Syntax.Concrete.Name Methods | |
| KillRange QName Source # | |
Defined in Mikan.Syntax.Concrete.Name Methods | |
| KillRange AppInfo Source # | |
Defined in Mikan.Syntax.Info Methods | |
| KillRange ConPatInfo Source # | |
Defined in Mikan.Syntax.Info Methods | |
| KillRange DeclInfo Source # | |
Defined in Mikan.Syntax.Info Methods | |
| KillRange ExprInfo Source # | |
Defined in Mikan.Syntax.Info Methods | |
| KillRange LHSInfo Source # | |
Defined in Mikan.Syntax.Info Methods | |
| KillRange LetInfo Source # | |
Defined in Mikan.Syntax.Info Methods | |
| KillRange MetaInfo Source # | |
Defined in Mikan.Syntax.Info Methods | |
| KillRange ModuleInfo Source # | |
Defined in Mikan.Syntax.Info Methods | |
| KillRange MutualInfo Source # | |
Defined in Mikan.Syntax.Info Methods | |
| KillRange PatInfo Source # | |
Defined in Mikan.Syntax.Info Methods | |
| KillRange Clause Source # | |
Defined in Mikan.Syntax.Internal.Clause Methods | |
| KillRange ClauseRecursive Source # | |
Defined in Mikan.Syntax.Internal.Clause Methods | |
| KillRange ConPatternInfo Source # | |
Defined in Mikan.Syntax.Internal.Pattern Methods | |
| KillRange DBPatVar Source # | |
Defined in Mikan.Syntax.Internal.Pattern Methods | |
| KillRange PatOrigin Source # | |
Defined in Mikan.Syntax.Internal.Pattern Methods | |
| KillRange PatternInfo Source # | |
Defined in Mikan.Syntax.Internal.Pattern Methods | |
| KillRange Substitution Source # | |
Defined in Mikan.Syntax.Internal.Term Methods | |
| KillRange Term Source # | |
Defined in Mikan.Syntax.Internal.Term Methods | |
| KillRange Literal Source # | |
Defined in Mikan.Syntax.Literal Methods | |
| KillRange ParseError Source # | |
Defined in Mikan.Syntax.Parser.Monad Methods | |
| KillRange Range Source # | |
Defined in Mikan.Syntax.Position Methods | |
| KillRange ScopeInfo Source # | |
Defined in Mikan.Syntax.Scope.Base Methods | |
| KillRange RawTopLevelModuleName Source # | |
Defined in Mikan.Syntax.TopLevelModuleName Methods | |
| KillRange CompiledClauses Source # | |
Defined in Mikan.TypeChecking.CompiledClause Methods | |
| KillRange SplitPatVar Source # | |
Defined in Mikan.TypeChecking.Coverage.SplitPattern Methods | |
| KillRange SplitTag Source # | |
Defined in Mikan.TypeChecking.Coverage.SplitTree Methods | |
| KillRange BuiltinSort Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange CompKit Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange CompiledRepresentation Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange Definition Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange Definitions Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange Defn Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange DisplayForm Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange DisplayTerm Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange DoGeneralize Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange EtaEquality Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange ExtLamInfo Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange FunctionFlag Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange InstanceInfo Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange InstanceTable Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange IsForced Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange MutualId Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange NumGeneralizableArgs Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange ProjLams Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange Projection Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange ProjectionLikenessMissing Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange Section Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange Sections Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange Signature Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange System Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange TermHead Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange WithFunInfo Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange Polarity Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| KillRange Occurrence Source # | |
Defined in Mikan.TypeChecking.Positivity.Occurrence Methods | |
| KillRange Permutation Source # | |
Defined in Mikan.Syntax.Position Methods | |
| KillRange Void Source # | |
Defined in Mikan.Syntax.Position Methods | |
| KillRange Text Source # | |
Defined in Mikan.Syntax.Position Methods | |
| KillRange ShortText Source # | |
Defined in Mikan.Syntax.Position Methods | |
| KillRange Integer Source # | |
Defined in Mikan.Syntax.Position Methods | |
| KillRange String Source # | Overlaps with |
Defined in Mikan.Syntax.Position Methods | |
| KillRange () Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT () Source # | |
| KillRange Bool Source # | |
Defined in Mikan.Syntax.Position Methods | |
| KillRange Int Source # | |
Defined in Mikan.Syntax.Position Methods | |
| KillRange a => KillRange (Binder' a) Source # | |
Defined in Mikan.Syntax.Abstract Methods killRange :: KillRangeT (Binder' a) Source # | |
| KillRange a => KillRange (Clause' a) Source # | |
Defined in Mikan.Syntax.Abstract Methods killRange :: KillRangeT (Clause' a) Source # | |
| KillRange e => KillRange (LHSCore' e) Source # | |
Defined in Mikan.Syntax.Abstract Methods killRange :: KillRangeT (LHSCore' e) Source # | |
| KillRange e => KillRange (Pattern' e) Source # | |
Defined in Mikan.Syntax.Abstract Methods killRange :: KillRangeT (Pattern' e) Source # | |
| KillRange a => KillRange (Arg a) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (Arg a) Source # | |
| KillRange a => KillRange (HasEta' a) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (HasEta' a) Source # | |
| KillRange a => KillRange (MaybePlaceholder a) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (MaybePlaceholder a) Source # | |
| KillRange (Ranged a) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (Ranged a) Source # | |
| KillRange a => KillRange (RecordDirectives' a) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (RecordDirectives' a) Source # | |
| KillRange a => KillRange (WithHiding a) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (WithHiding a) Source # | |
| KillRange a => KillRange (WithOrigin a) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (WithOrigin a) Source # | |
| KillRange a => KillRange (FieldAssignment' a) Source # | |
Defined in Mikan.Syntax.Concrete Methods killRange :: KillRangeT (FieldAssignment' a) Source # | |
| KillRange e => KillRange (OpApp e) Source # | |
Defined in Mikan.Syntax.Concrete Methods killRange :: KillRangeT (OpApp e) Source # | |
| KillRange (TacticAttribute' a) Source # | |
Defined in Mikan.Syntax.Concrete Methods killRange :: KillRangeT (TacticAttribute' a) Source # | |
| KillRange x => KillRange (ThingWithFixity x) Source # | |
Defined in Mikan.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) Source # | |
| KillRange (DefInfo' t) Source # | |
Defined in Mikan.Syntax.Info Methods killRange :: KillRangeT (DefInfo' t) Source # | |
| KillRange a => KillRange (Abs a) Source # | |
Defined in Mikan.Syntax.Internal.Dom Methods killRange :: KillRangeT (Abs a) Source # | |
| KillRange a => KillRange (Elim' a) Source # | |
Defined in Mikan.Syntax.Internal.Elim Methods killRange :: KillRangeT (Elim' a) Source # | |
| KillRange a => KillRange (Pattern' a) Source # | |
Defined in Mikan.Syntax.Internal.Pattern Methods killRange :: KillRangeT (Pattern' a) Source # | |
| KillRange a => KillRange (Tele a) Source # | |
Defined in Mikan.Syntax.Internal.Telescope Methods killRange :: KillRangeT (Tele a) Source # | |
| KillRange a => KillRange (Blocked a) Source # | |
Defined in Mikan.Syntax.Internal.Term Methods killRange :: KillRangeT (Blocked a) Source # | |
| KillRange a => KillRange (Level' a) Source # | |
Defined in Mikan.Syntax.Internal.Term Methods killRange :: KillRangeT (Level' a) Source # | |
| KillRange a => KillRange (PlusLevel' a) Source # | |
Defined in Mikan.Syntax.Internal.Term Methods killRange :: KillRangeT (PlusLevel' a) Source # | |
| KillRange a => KillRange (Sort' a) Source # | |
Defined in Mikan.Syntax.Internal.Term Methods killRange :: KillRangeT (Sort' a) Source # | |
| KillRange a => KillRange (PrintRange a) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (PrintRange a) Source # | |
| KillRange (TopLevelModuleName' Range) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (TopLevelModuleName' Range) Source # | |
| KillRange c => KillRange (Case c) Source # | |
Defined in Mikan.TypeChecking.CompiledClause Methods killRange :: KillRangeT (Case c) Source # | |
| KillRange c => KillRange (WithArity c) Source # | |
Defined in Mikan.TypeChecking.CompiledClause Methods killRange :: KillRangeT (WithArity c) Source # | |
| KillRange a => KillRange (SplitTree' a) Source # | |
Defined in Mikan.TypeChecking.Coverage.SplitTree Methods killRange :: KillRangeT (SplitTree' a) Source # | |
| (KillRange a, Ord a) => KillRange (DiscrimTree a) Source # | |
Defined in Mikan.TypeChecking.DiscrimTree.Types Methods killRange :: KillRangeT (DiscrimTree a) Source # | |
| KillRange (Closure a) Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods killRange :: KillRangeT (Closure a) Source # | |
| KillRange c => KillRange (FunctionInverse' c) Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods killRange :: KillRangeT (FunctionInverse' c) Source # | |
| KillRange a => KillRange (Open a) Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods killRange :: KillRangeT (Open a) Source # | |
| KillRange a => KillRange (List1 a) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (List1 a) Source # | |
| KillRange a => KillRange (List2 a) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (List2 a) Source # | |
| KillRange a => KillRange (Drop a) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (Drop a) Source # | |
| (Ord a, KillRange a) => KillRange (Set1 a) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (Set1 a) Source # | |
| KillRange (SmallSet FunctionFlag) Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| (Ord a, KillRange a) => KillRange (Set a) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (Set a) Source # | |
| KillRange a => KillRange (Maybe a) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (Maybe a) Source # | |
| KillRange a => KillRange (Maybe a) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (Maybe a) Source # | |
| KillRange a => KillRange [a] Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT [a] Source # | |
| (KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (ImportDirective' a b) Source # | |
| (KillRange a, KillRange b) => KillRange (ImportedName' a b) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (ImportedName' a b) Source # | |
| (KillRange name, KillRange a) => KillRange (Named name a) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (Named name a) Source # | |
| (KillRange a, KillRange b) => KillRange (Renaming' a b) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (Renaming' a b) Source # | |
| (KillRange a, KillRange b) => KillRange (Using' a b) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (Using' a b) Source # | |
| (KillRange t, KillRange a) => KillRange (Dom' t a) Source # | |
Defined in Mikan.Syntax.Internal.Dom Methods killRange :: KillRangeT (Dom' t a) Source # | |
| (KillRange a, KillRange b) => KillRange (Type'' a b) Source # | |
Defined in Mikan.Syntax.Internal.Term Methods killRange :: KillRangeT (Type'' a b) Source # | |
| KillRange a => KillRange (Map1 k a) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (Map1 k a) Source # | |
| KillRange a => KillRange (Map k a) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (Map k a) Source # | |
| (KillRange a, KillRange b) => KillRange (Either a b) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (Either a b) Source # | |
| (KillRange a, KillRange b) => KillRange (a, b) Source # | |
Defined in Mikan.Syntax.Position Methods killRange :: KillRangeT (a, b) Source # | |
| (KillRange a, KillRange b, KillRange c) => KillRange (a, b, c) Source # | |
Defined in Mikan.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 Mikan.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 Mikan.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.
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 :: Range' a -> Range' a -> Range' a Source #
fuseRanges r r' unions the ranges r and r'.
Meaning it finds the least range r0 that covers r and r'.
Precondition: The ranges must point to the same file (or be empty).
beginningOf :: Range -> Range Source #
beginningOf r is an empty range (a single, empty interval)
positioned at the beginning of r. If r does not have a
beginning, then noRange is returned.
beginningOfFile :: BeginningOfFile a => a -> Range Source #
Return an empty range (a single, empty interval) at the beginning of the file.
interleaveRanges :: HasRangeWithoutFile a => [a] -> [a] -> ([a], [(a, a)]) Source #
Interleaves two streams of ranged elements
It will report the conflicts as a list of conflicting pairs. In case of conflict, the element with the earliest start position is placed first. In case of a tie, the element with the earliest ending position is placed first. If both tie, the element from the first list is placed first.