Safe Haskell	None
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 IntMaps 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

NFData a => NFData (PairInt a) Source #
Instance details Defined in Agda.Utils.RangeMap Methods rnf :: PairInt a -> ()
Show a => Show (PairInt a) Source #
Instance details Defined in Agda.Utils.RangeMap Methods showsPrec :: Int -> PairInt a -> ShowS show :: PairInt a -> String showList :: [PairInt a] -> ShowS

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

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 Word32 Source # icod_ :: RangeMap a -> S Word32 Source # value :: Word32 -> 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 #
NFData a => NFData (RangeMap a) Source #
Instance details Defined in Agda.Utils.RangeMap Methods rnf :: RangeMap a -> ()
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 mappend :: RangeMap a -> RangeMap a -> RangeMap a mconcat :: [RangeMap a] -> RangeMap a
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 # sconcat :: NonEmpty (RangeMap a) -> RangeMap a stimes :: Integral b => b -> RangeMap a -> RangeMap a
Show a => Show (RangeMap a) Source #
Instance details Defined in Agda.Utils.RangeMap Methods showsPrec :: Int -> RangeMap a -> ShowS show :: RangeMap a -> String showList :: [RangeMap a] -> ShowS
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.