Agda.Utils.RangeMap

Maps containing non-overlapping intervals.

Documentation

class IsBasicRangeMap a m | m -> a where

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

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

toMap :: m -> IntMap a

Converts range maps to IntMaps from positions to values.

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

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

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

IsBasicRangeMap Aspects PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> PositionMap

toMap :: PositionMap -> IntMap Aspects

toList :: PositionMap -> [(Range, Aspects)]

coveringRange :: PositionMap -> Maybe Range

IsBasicRangeMap Aspects RangePair

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> RangePair

toMap :: RangePair -> IntMap Aspects

toList :: RangePair -> [(Range, Aspects)]

coveringRange :: RangePair -> Maybe Range

IsBasicRangeMap Aspects (DelayedMerge PositionMap)

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge PositionMap

toMap :: DelayedMerge PositionMap -> IntMap Aspects

toList :: DelayedMerge PositionMap -> [(Range, Aspects)]

coveringRange :: DelayedMerge PositionMap -> Maybe Range

IsBasicRangeMap Aspects (DelayedMerge RangePair)

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge RangePair

toMap :: DelayedMerge RangePair -> IntMap Aspects

toList :: DelayedMerge RangePair -> [(Range, Aspects)]

coveringRange :: DelayedMerge RangePair -> Maybe Range

Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a))

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> a -> DelayedMerge (RangeMap a)

toMap :: DelayedMerge (RangeMap a) -> IntMap a

toList :: DelayedMerge (RangeMap a) -> [(Range, a)]

coveringRange :: DelayedMerge (RangeMap a) -> Maybe Range

IsBasicRangeMap a (RangeMap a)

Defined in Agda.Utils.RangeMap

Methods

singleton :: Ranges -> a -> RangeMap a

toMap :: RangeMap a -> IntMap a

toList :: RangeMap a -> [(Range, a)]

coveringRange :: RangeMap a -> Maybe Range

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

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

newtype PairInt a

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

EmbPrj a => EmbPrj (PairInt a)

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: PairInt a -> S Int32

icod_ :: PairInt a -> S Int32

value :: Int32 -> R (PairInt a)

Show a => Show (PairInt a)

Defined in Agda.Utils.RangeMap

Methods

showsPrec :: Int -> PairInt a -> ShowS

show :: PairInt a -> String

showList :: [PairInt a] -> ShowS

NFData a => NFData (PairInt a)

Defined in Agda.Utils.RangeMap

Methods

rnf :: PairInt a -> ()

newtype RangeMap a

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

Convert PositionMap (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: PositionMap -> RangeMap Aspects

Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a))

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> a -> DelayedMerge (RangeMap a)

toMap :: DelayedMerge (RangeMap a) -> IntMap a

toList :: DelayedMerge (RangeMap a) -> [(Range, a)]

coveringRange :: DelayedMerge (RangeMap a) -> Maybe Range

IsBasicRangeMap a (RangeMap a)

Defined in Agda.Utils.RangeMap

Methods

singleton :: Ranges -> a -> RangeMap a

toMap :: RangeMap a -> IntMap a

toList :: RangeMap a -> [(Range, a)]

coveringRange :: RangeMap a -> Maybe Range

EmbPrj a => EmbPrj (RangeMap a)

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: RangeMap a -> S Int32

icod_ :: RangeMap a -> S Int32

value :: Int32 -> R (RangeMap a)

Null (RangeMap a)

Defined in Agda.Utils.RangeMap

Methods

empty :: RangeMap a

null :: RangeMap a -> Bool

Semigroup a => Monoid (RangeMap a)

Merges RangeMaps by inserting every "piece" of the smaller one into the larger one.

Defined in Agda.Utils.RangeMap

Methods

mempty :: RangeMap a

mappend :: RangeMap a -> RangeMap a -> RangeMap a

mconcat :: [RangeMap a] -> RangeMap a

Semigroup a => Semigroup (RangeMap a)

Merges RangeMaps by inserting every "piece" of the smaller one into the larger one.

Defined in Agda.Utils.RangeMap

Methods

(<>) :: RangeMap a -> RangeMap a -> RangeMap a

sconcat :: NonEmpty (RangeMap a) -> RangeMap a

stimes :: Integral b => b -> RangeMap a -> RangeMap a

Show a => Show (RangeMap a)

Defined in Agda.Utils.RangeMap

Methods

showsPrec :: Int -> RangeMap a -> ShowS

show :: RangeMap a -> String

showList :: [RangeMap a] -> ShowS

NFData a => NFData (RangeMap a)

Defined in Agda.Utils.RangeMap

Methods

rnf :: RangeMap a -> ()

Convert (DelayedMerge PositionMap) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge PositionMap -> RangeMap Aspects

Convert (DelayedMerge RangePair) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> RangeMap Aspects

Convert (RangeMap Aspects) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: RangeMap Aspects -> RangeMap Aspects

rangeMapInvariant :: RangeMap a -> Bool

Invariant for RangeMap.

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

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

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

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)

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)

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

restrictTo :: Range -> RangeMap a -> RangeMap a

Restricts the RangeMap to the given range.