Idris2Doc : Text.Bounds

Text.Bounds

(source)
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
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
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