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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Utils.RangeMap

Description

Maps containing non-overlapping intervals.

Synopsis

- class IsBasicRangeMap a m | m -> a where
  - singleton :: Ranges -> a -> m
  - toMap :: m -> IntMap a
  - toList :: m -> [(Range, a)]
  - coveringRange :: m -> Maybe Range
- several :: (IsBasicRangeMap a hl, Monoid hl) => [Ranges] -> a -> hl
- newtype PairInt a = PairInt (Pair Int a)
- newtype RangeMap a = RangeMap {
  - rangeMap :: Map Int (PairInt a)
  }
- rangeMapInvariant :: RangeMap a -> Bool
- fromNonOverlappingNonEmptyAscendingList :: [(Range, a)] -> RangeMap a
- insert :: (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
- splitAt :: Int -> RangeMap a -> (RangeMap a, RangeMap a)
- insideAndOutside :: Range -> RangeMap a -> (RangeMap a, RangeMap a)
- restrictTo :: Range -> RangeMap a -> RangeMap a

# Documentation

class IsBasicRangeMap a m | m -> a where Source #

A class that is intended to make it easy to swap between different range map implementations.

Note that some `RangeMap` operations are not included in this class.

Minimal complete definition

singleton, toMap, toList

Methods

singleton :: Ranges -> a -> m Source #

The map ``singleton` rs x` contains the ranges from `rs`, and every position in those ranges is associated with `x`.

toMap :: m -> IntMap a Source #

Converts range maps to `IntMap`s from positions to values.

toList :: m -> [(Range, a)] Source #

Converts the map to a list. The ranges are non-overlapping and non-empty, and earlier ranges precede later ones in the list.

coveringRange :: m -> Maybe Range Source #

Returns the smallest range covering everything in the map (or `Nothing`, if the range would be empty).

Note that the default implementation of this operation might be inefficient.

#### Instances

Instances details

IsBasicRangeMap Aspects PositionMap Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> PositionMap Source # toMap :: PositionMap -> IntMap Aspects Source # toList :: PositionMap -> [(Range, Aspects)] Source # coveringRange :: PositionMap -> Maybe Range Source #
IsBasicRangeMap Aspects RangePair Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> RangePair Source # toMap :: RangePair -> IntMap Aspects Source # toList :: RangePair -> [(Range, Aspects)] Source # coveringRange :: RangePair -> Maybe Range Source #
IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge PositionMap Source # toMap :: DelayedMerge PositionMap -> IntMap Aspects Source # toList :: DelayedMerge PositionMap -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge PositionMap -> Maybe Range Source #
IsBasicRangeMap Aspects (DelayedMerge RangePair) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge RangePair Source # toMap :: DelayedMerge RangePair -> IntMap Aspects Source # toList :: DelayedMerge RangePair -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge RangePair -> Maybe Range Source #
Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a)) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> a -> DelayedMerge (RangeMap a) Source # toMap :: DelayedMerge (RangeMap a) -> IntMap a Source # toList :: DelayedMerge (RangeMap a) -> [(Range, a)] Source # coveringRange :: DelayedMerge (RangeMap a) -> Maybe Range Source #
IsBasicRangeMap a (RangeMap a) Source # |
Instance details Defined in Agda.Utils.RangeMap Methods singleton :: Ranges -> a -> RangeMap a Source # toMap :: RangeMap a -> IntMap a Source # toList :: RangeMap a -> [(Range, a)] Source # coveringRange :: RangeMap a -> Maybe Range Source #

several :: (IsBasicRangeMap a hl, Monoid hl) => [Ranges] -> a -> hl Source #

Like `singleton`, but with several `Ranges` instead of only one.

newtype PairInt a Source #

A strict pair type where the first argument must be an `Int`.

This type is included because there is no `NFData` instance for `Pair` in the package `strict` before version 4.

Constructors

PairInt (Pair Int a) |

#### Instances

Instances details

EmbPrj a => EmbPrj (PairInt a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: PairInt a -> S Int32 Source # icod_ :: PairInt a -> S Int32 Source # value :: Int32 -> R (PairInt a) Source #
Show a => Show (PairInt a) Source # |
Instance details Defined in Agda.Utils.RangeMap Methods showsPrec :: Int -> PairInt a -> ShowS Source # show :: PairInt a -> String Source # showList :: [PairInt a] -> ShowS Source #
NFData a => NFData (PairInt a) Source # |
Instance details Defined in Agda.Utils.RangeMap Methods rnf :: PairInt a -> () Source #

newtype RangeMap a Source #

Maps containing non-overlapping intervals.

The implementation does not use IntMap, because IntMap does not come with a constant-time size function.

Note the invariant which `RangeMap`s should satisfy (`rangeMapInvariant`).

Constructors

RangeMap |

Fields

- rangeMap :: Map Int (PairInt a)

  The keys are starting points of ranges, and the pairs contain endpoints and values.

#### Instances

Instances details

Convert PositionMap (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: PositionMap -> RangeMap Aspects Source #
Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a)) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> a -> DelayedMerge (RangeMap a) Source # toMap :: DelayedMerge (RangeMap a) -> IntMap a Source # toList :: DelayedMerge (RangeMap a) -> [(Range, a)] Source # coveringRange :: DelayedMerge (RangeMap a) -> Maybe Range Source #
IsBasicRangeMap a (RangeMap a) Source # |
Instance details Defined in Agda.Utils.RangeMap Methods singleton :: Ranges -> a -> RangeMap a Source # toMap :: RangeMap a -> IntMap a Source # toList :: RangeMap a -> [(Range, a)] Source # coveringRange :: RangeMap a -> Maybe Range Source #
EmbPrj a => EmbPrj (RangeMap a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: RangeMap a -> S Int32 Source # icod_ :: RangeMap a -> S Int32 Source # value :: Int32 -> R (RangeMap a) Source #
Null (RangeMap a) Source # |
Instance details Defined in Agda.Utils.RangeMap Methods empty :: RangeMap a Source # null :: RangeMap a -> Bool Source #
Semigroup a => Monoid (RangeMap a) Source # | Merges `RangeMap`s by inserting every "piece" of the smaller one into the larger one.
Instance details Defined in Agda.Utils.RangeMap Methods mempty :: RangeMap a Source # mappend :: RangeMap a -> RangeMap a -> RangeMap a Source # mconcat :: [RangeMap a] -> RangeMap a Source #
Semigroup a => Semigroup (RangeMap a) Source # | Merges `RangeMap`s by inserting every "piece" of the smaller one into the larger one.
Instance details Defined in Agda.Utils.RangeMap Methods (<>) :: RangeMap a -> RangeMap a -> RangeMap a Source # sconcat :: NonEmpty (RangeMap a) -> RangeMap a Source # stimes :: Integral b => b -> RangeMap a -> RangeMap a Source #
Show a => Show (RangeMap a) Source # |
Instance details Defined in Agda.Utils.RangeMap Methods showsPrec :: Int -> RangeMap a -> ShowS Source # show :: RangeMap a -> String Source # showList :: [RangeMap a] -> ShowS Source #
NFData a => NFData (RangeMap a) Source # |
Instance details Defined in Agda.Utils.RangeMap Methods rnf :: RangeMap a -> () Source #
Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge PositionMap -> RangeMap Aspects Source #
Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> RangeMap Aspects Source #
Convert (RangeMap Aspects) (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: RangeMap Aspects -> RangeMap Aspects Source #

rangeMapInvariant :: RangeMap a -> Bool Source #

Invariant for `RangeMap`.

The ranges must not be empty, and they must not overlap.

fromNonOverlappingNonEmptyAscendingList :: [(Range, a)] -> RangeMap a Source #

Converts a list of pairs of ranges and values to a `RangeMap`. The ranges have to be non-overlapping and non-empty, and earlier ranges have to precede later ones.

insert :: (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a Source #

Inserts a value, along with a corresponding `Range`, into a `RangeMap`. No attempt is made to merge adjacent ranges with equal values.

The function argument is used to combine values. The inserted value is given as the first argument to the function.

splitAt :: Int -> RangeMap a -> (RangeMap a, RangeMap a) Source #

The value of ``splitAt` p f` is a pair `(f1, f2)` which contains everything from `f`. All the positions in `f1` are less than `p`, and all the positions in `f2` are greater than or equal to `p`.

insideAndOutside :: Range -> RangeMap a -> (RangeMap a, RangeMap a) Source #

Returns a `RangeMap` overlapping the given range, as well as the rest of the map.

restrictTo :: Range -> RangeMap a -> RangeMap a Source #

Restricts the `RangeMap` to the given range.