Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Utils.RangeMap

Description

Maps containing non-overlapping intervals.

Synopsis

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

IsBasicRangeMap Aspects RangePair Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

IsBasicRangeMap Aspects (DelayedMerge RangePair) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a)) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

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

NFData a => NFData (PairInt a) Source # 
Instance details

Defined in Agda.Utils.RangeMap

Methods

rnf :: PairInt a -> ()

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

Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a)) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

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 RangeMaps by inserting every "piece" of the smaller one into the larger one.

Instance details

Defined in Agda.Utils.RangeMap

Semigroup a => Semigroup (RangeMap a) Source #

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

NFData a => NFData (RangeMap a) Source # 
Instance details

Defined in Agda.Utils.RangeMap

Methods

rnf :: RangeMap a -> ()

Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Convert (RangeMap Aspects) (RangeMap Aspects) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

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.