Data.String.Position

A small library introducing string positions
This can be used as an alternative to unpacking a string into a list of
characters

Definitions

record ValidPosition : String -> Type

  @ValidPosition points to an existing character into
  @str  its parameter string
  Do NOT publicly export so that users cannot manufacture arbitrary positions

Totality: total
Visibility: export
Constructor: 

MkValidPosition : Int -> Int -> ValidPosition str

Projections:

.currentIndex : ValidPosition str -> Int

  @currentIndex is the valid position into str

.parameterLength : ValidPosition str -> Int

  @parameterLength is the length of the parameter str

Position : String -> Type

  A position is either a ValidPosition or the end of the string

Totality: total
Visibility: public export

mkPosition : (str : String) -> Int -> Position str

  Manufacture a position by checking it is strictly inside the string

Totality: total
Visibility: export

mvPosition : ValidPosition str -> Int -> Position str

  Move a position (note that we do not need access to the string here)

Totality: total
Visibility: export

init : (str : String) -> Position str

  Find the initial position inside the input string

Totality: total
Visibility: export

next : ValidPosition str -> Position str

  Move from a valid position to the next position in the string

Totality: total
Visibility: export

index : ValidPosition str -> Char

  We can safely access the character at a valid position

Totality: total
Visibility: export

uncons : ValidPosition str -> (Char, Position str)

  We can successfully uncons the substring starting at a `ValidPosition`.
  Note that we can use `map uncons pos` to uncons the substring starting
  a `Position`.

Totality: total
Visibility: export

span : (Char -> Bool) -> Position str -> Position str

  @span keeps munching characters of the substring starting at a given
  position as long as the predicate is true of them. It returns the position
  after the last successful munch.
  Using `subString` to recover the string selected by `span` should yield
  the same result as Data.String's `span`. That is to say we should have:
  ```
  subString pos (Position.span p pos) = String.span p (subString pos Nothing)
  ```

Totality: total
Visibility: export

count : (Char -> Bool) -> Position str -> Nat

  @count computes the length of the substring one would obtain if one were
  to filter out characters based on the predicate passed as an argument.
  It replaces the `length (filter p (fastUnpack str))` pattern.

Totality: total
Visibility: export

distance : Position str -> Position str -> Int

  Distance between a starting position and an end one.
  We assume that the end position is *after* the starting one, otherwise the
  output may be negative.

Totality: total
Visibility: export

subString : Position str -> Position str -> String

  the substring of length `distance start end` that is contained between
  start (inclusive) and end (exclusive).

Totality: total
Visibility: export