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

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Highlighting.Range

Description

Ranges.

Synopsis

- data Range = Range {
  - from :: !Int
  - to :: !Int
  }
- rangeInvariant :: Range -> Bool
- newtype Ranges = Ranges [Range]
- rangesInvariant :: Ranges -> Bool
- overlapping :: Range -> Range -> Bool
- overlappings :: Ranges -> Ranges -> Bool
- empty :: Null a => a
- rangeToPositions :: Range -> [Int]
- rangesToPositions :: Ranges -> [Int]
- rToR :: Range -> Ranges
- rangeToRange :: Range -> Range
- minus :: Ranges -> Ranges -> Ranges

# Documentation

data Range Source #

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 :: !Int
- to :: !Int

#### Instances

Instances details

EmbPrj Range Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Range -> S Word32 Source # icod_ :: Range -> S Word32 Source # value :: Word32 -> R Range Source #
Null Range Source # |
Instance details Defined in Agda.Interaction.Highlighting.Range Methods empty :: Range Source # null :: Range -> Bool Source #
NFData Range Source # |
Instance details Defined in Agda.Interaction.Highlighting.Range Methods rnf :: Range -> () Source #
Show Range Source # |
Instance details Defined in Agda.Interaction.Highlighting.Range Methods showsPrec :: Int -> Range -> ShowS Source # show :: Range -> String Source # showList :: [Range] -> ShowS Source #
Eq Range Source # |
Instance details Defined in Agda.Interaction.Highlighting.Range Methods (==) :: Range -> Range -> Bool Source # (/=) :: Range -> Range -> Bool Source #
Ord Range Source # |
Instance details Defined in Agda.Interaction.Highlighting.Range Methods compare :: Range -> Range -> Ordering Source # (<) :: Range -> Range -> Bool Source # (<=) :: Range -> Range -> Bool Source # (>) :: Range -> Range -> Bool Source # (>=) :: Range -> Range -> Bool Source # max :: Range -> Range -> Range Source # min :: Range -> Range -> Range Source #

rangeInvariant :: Range -> Bool Source #

The `Range` invariant.

newtype Ranges Source #

Zero or more consecutive and separated ranges.

Constructors

Ranges [Range] |

#### Instances

Instances details

NFData Ranges Source # |
Instance details Defined in Agda.Interaction.Highlighting.Range Methods rnf :: Ranges -> () Source #
Show Ranges Source # |
Instance details Defined in Agda.Interaction.Highlighting.Range Methods showsPrec :: Int -> Ranges -> ShowS Source # show :: Ranges -> String Source # showList :: [Ranges] -> ShowS Source #
Eq Ranges Source # |
Instance details Defined in Agda.Interaction.Highlighting.Range Methods (==) :: Ranges -> Ranges -> Bool Source # (/=) :: Ranges -> Ranges -> Bool Source #

rangesInvariant :: Ranges -> Bool Source #

The `Ranges` invariant.

overlapping :: Range -> Range -> Bool Source #

`True` iff the ranges overlap.

The ranges are assumed to be well-formed.

overlappings :: Ranges -> Ranges -> Bool Source #

empty :: Null a => a Source #

rangeToPositions :: Range -> [Int] Source #

Converts a range to a list of positions.

rangesToPositions :: Ranges -> [Int] Source #

Converts several ranges to a list of positions.

rToR :: Range -> Ranges Source #

Converts a `Range` to a `Ranges`.

rangeToRange :: Range -> Range Source #

Converts a `Range`, seen as a continuous range, to a `Range`.

minus :: Ranges -> Ranges -> Ranges Source #

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