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

Safe Haskell | None

Agda.Interaction.Highlighting.Range

Description

Ranges.

Synopsis

- data Range = Range {
  - from :: Integer
  - to :: Integer
  }
- rangeInvariant :: Range -> Bool
- newtype Ranges = Ranges [Range]
- rangesInvariant :: Ranges -> Bool
- overlapping :: Range -> Range -> Bool
- empty :: Range -> Bool
- rangeToPositions :: Range -> [Integer]
- rangesToPositions :: Ranges -> [Integer]
- rToR :: Range -> Ranges
- minus :: Ranges -> Ranges -> Ranges
- tests :: IO Bool

# Documentation

data Range

Character ranges. The first character in the file has position 1. Note that the `to` position is considered to be outside of the range.

Invariant: ``from` `<=` `to``.

Constructors

Range |

Fields

from :: Integer
to :: Integer

Instances

Eq Range |
Ord Range |
Show Range |
Typeable Range |
Arbitrary Range |
CoArbitrary Range |
EmbPrj Range |

rangeInvariant :: Range -> Bool

The `Range` invariant.

newtype Ranges

Zero or more consecutive and separated ranges.

Constructors

Ranges [Range] |

Instances

Eq Ranges |
Show Ranges |
Arbitrary Ranges |

rangesInvariant :: Ranges -> Bool

The `Ranges` invariant.

overlapping :: Range -> Range -> Bool

`True` iff the ranges overlap.

The ranges are assumed to be well-formed.

empty :: Range -> Bool

`True` iff the range is empty.

rangeToPositions :: Range -> [Integer]

Converts a range to a list of positions.

rangesToPositions :: Ranges -> [Integer]

Converts several ranges to a list of positions.

rToR :: Range -> Ranges

Converts a `Range` to a `Ranges`.

minus :: Ranges -> Ranges -> Ranges

`minus xs ys` computes the difference between `xs` and `ys`: the result contains those positions which are present in `xs` but not in `ys`.

Linear in the lengths of the input ranges.

tests :: IO Bool

All the properties.