Libraries.Data.PosMap

Specialized implementation of an interval map with finger trees [1].
This data structure is meant to get efficiently data with a correlated NonEmptyFC.
The element data type must implement the `Measure` interface. An implementation
is provided already for NonEmptyFC and tuples with NonEmptyFC as first element.

[1] https://www.staff.city.ac.uk/~ross/papers/FingerTree.pdf

Definitions

FileRange : Type

Totality: total
Visibility: public export

interface Measure : Type -> Type

  Things that have an associated interval in the source files.

Parameters: a
Methods:

measure : a -> FileRange

Implementations:

Measure NonEmptyFC

Measure (NonEmptyFC, a)

measure : Measure a => a -> FileRange

Totality: total
Visibility: public export

map : MeasureRM b => (a -> b) -> Node a -> Node b

Totality: total
Visibility: export

traverse : (Applicative f, MeasureRM b) => (a -> f b) -> Node a -> f (Node b)

Totality: total
Visibility: export

data PosMap : Type -> Type

Totality: total
Visibility: export
Constructors:

Empty : PosMap a

Single : a -> PosMap a

Deep : RMFileRange -> Digit a -> PosMap (Node a) -> Digit a -> PosMap a

Hints:

Foldable PosMap

Show a => Show (PosMap a)

(TTC a, Measure a) => TTC (PosMap a)

empty : PosMap a

Totality: total
Visibility: export

singleton : a -> PosMap a

Totality: total
Visibility: export

map : MeasureRM b => (a -> b) -> PosMap a -> PosMap b

Totality: total
Visibility: export

traverse : (Applicative f, MeasureRM b) => (a -> f b) -> PosMap a -> f (PosMap b)

Totality: total
Visibility: export

takeUntil : MeasureRM a => (Interval -> Bool) -> PosMap a -> PosMap a

Totality: total
Visibility: export

dropUntil : MeasureRM a => (Interval -> Bool) -> PosMap a -> PosMap a

Totality: total
Visibility: export

insert : Measure a => a -> PosMap a -> PosMap a

  Inserts a new element in the map, in lexicographical order.

Totality: total
Visibility: export

fromList : Measure a => List a -> PosMap a

  Builds a new map from a list of measurable elements, inserting in
  lexicographical order.

Totality: total
Visibility: export

union : Measure a => PosMap a -> PosMap a -> PosMap a

  Merges two interval maps.

Totality: total
Visibility: export

inRange : MeasureRM a => FilePos -> FilePos -> PosMap a -> List a

  Finds all the intervals that overlap with the given interval.

Totality: total
Visibility: export

exactRange : MeasureRM a => FilePos -> FilePos -> PosMap a -> List a

  Finds the values matching the exact interval input

Totality: total
Visibility: export

searchPos : MeasureRM a => FilePos -> PosMap a -> List a

  Returns all the interval that contains the given point.

Totality: total
Visibility: export

intersections : MeasureRM a => FileRange -> PosMap a -> List a

  Returns all the intervals that intersect the given interval.

Totality: total
Visibility: export

dominators : MeasureRM a => FileRange -> PosMap a -> List a

  Returns all the intervals that contain the given interval.

Totality: total
Visibility: export

bounds : Measure a => PosMap a -> Maybe FileRange

  Returns the extreme boundaries of the map, if non empty.

Totality: total
Visibility: export