Text.Bounds

Definitions

record Position : Type

  Position in a string as a pair of natural numbers.
  Both numbers are zero-based.

Totality: total
Visibility: public export
Constructor: 

P : Nat -> Nat -> Position

Projections:

.col : Position -> Nat

  The current column in a string (0-based)

.line : Position -> Nat

  The current line in a string (0-based)

Hints:

Eq Position

Interpolation Position

Monoid Position

Ord Position

Semigroup Position

Show Position

.line : Position -> Nat

  The current line in a string (0-based)

Totality: total
Visibility: public export

line : Position -> Nat

  The current line in a string (0-based)

Totality: total
Visibility: public export

.col : Position -> Nat

  The current column in a string (0-based)

Totality: total
Visibility: public export

col : Position -> Nat

  The current column in a string (0-based)

Totality: total
Visibility: public export

begin : Position

  The beginning of a string. This is an alias for `P 0 0`.

Totality: total
Visibility: public export

incCol : Position -> Position

  Increase the current column by one.

Totality: total
Visibility: public export

incLine : Position -> Position

  Increase the current line by one, resetting the
  column to 0.

Totality: total
Visibility: public export

addCol : Nat -> Position -> Position

  Increase the current column by the given number of steps.

Totality: total
Visibility: public export

relativeTo : Position -> Position -> Position

  Computes `p2` relative to `p1`, that is, given an earlier
  position `p1`, returns the number of lines and columns
  necessary to advance from `p1` to `p2`.

Totality: total
Visibility: export

incString : String -> Position -> Position

  Advances the given text position by the characters encountered
  in the given string.
  
  A line feed character ('\n'; codepoint `0x0A`) will increase
  the current line by one and reset the column to zero. Every
  other character will increase the column by one.

Totality: total
Visibility: export

incByte : Bits8 -> Position -> Position

  Advances the given text position by one byte in a UTF-8 string.
  
  A line feed character (byte '0x0a') increases the line by one and
  resets the column to zero. The first byte of any other UTF-8 character
  increases the column by one. Any other UTF-8 byte leaves the
  position unchanged.

Totality: total
Visibility: export

incBytes : ByteString -> Position -> Position

  Advances the given text position by the bytes encountered
  in the given string.
  
  A line feed byte (`0x0A`) will increase
  the current line by one and reset the column to zero. Every
  other start character of a unicode code point will advance
  the column by one.

Totality: total
Visibility: export

positionMapFrom : Position -> ByteVect n -> IArray (S n) Position

  From a byte vector, generates an array that maps each
  byte index to the corresponding text position (line and column),
  starting from the given start position.
  
  The line number is increased after a line feed (`'\n'`) character.

Totality: total
Visibility: export

positionMap : ByteVect n -> IArray (S n) Position

  From a byte vector, generates an array that maps each
  byte index to the corresponding text position (line and column).
  
  The line number is increased after a line feed (`'\n'`) character.

Totality: total
Visibility: export

next : Char -> Position -> Position

  Adjusts the current position by one character.
  
  If the character is a line break, a new line will be strated and
  the column set to zero, otherwise, the column is increase by one.

Totality: total
Visibility: public export

data Bounds : Type

  A pair of `Position`s, describing a text range, or `NoBounds` for
  use - for instance - with programmatically created tokens.

Totality: total
Visibility: public export
Constructors:

BS : Position -> Position -> Bounds

NoBounds : Bounds

Hints:

Eq Bounds

Interpolation Bounds

Monoid Bounds

Semigroup Bounds

Show Bounds

relativeTo : Bounds -> Position -> Bounds

Totality: total
Visibility: export

oneChar : Position -> Bounds

  Convert a single `Position` to a range one character wide.

Totality: total
Visibility: public export

record Bounded : Type -> Type

  Pairs a value with the textual bounds from where it was parsed.

Totality: total
Visibility: public export
Constructor: 

B : ty -> Bounds -> Bounded ty

Projections:

.bounds : Bounded ty -> Bounds

.val : Bounded ty -> ty

Hints:

Applicative Bounded

Eq ty => Eq (Bounded ty)

FailParse (Either (Bounded (InnerError e))) e

Foldable Bounded

Functor Bounded

Monad Bounded

Show ty => Show (Bounded ty)

Traversable Bounded

.val : Bounded ty -> ty

Totality: total
Visibility: public export

val : Bounded ty -> ty

Totality: total
Visibility: public export

.bounds : Bounded ty -> Bounds

Totality: total
Visibility: public export

bounds : Bounded ty -> Bounds

Totality: total
Visibility: public export

bounded : a -> Position -> Position -> Bounded a

  Smart costructor for `Bounded`.

Totality: total
Visibility: public export

oneChar : a -> Position -> Bounded a

  Smart costructor for `Bounded`.

Totality: total
Visibility: public export

app : Bounded (a -> b) -> Bounded a -> Bounded b

  Implementation of `(<*>)`

Totality: total
Visibility: public export

bind : Bounded a -> (a -> Bounded b) -> Bounded b

  Implementation of `(>>=)`

Totality: total
Visibility: public export

fromPosition : Bounded a -> Position -> Bounded a

Totality: total
Visibility: export

noBounds : Bounded t -> Bounded t

Totality: total
Visibility: export