Idris2Doc : Data.String.Position

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
Position : String -> Type
  A position is either a ValidPosition or the end of the string

Totality: total
recordValidPosition : 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
Constructor: 
MkValidPosition : Int -> Int -> ValidPositionstr

Projections:
.currentIndex : ValidPositionstr -> Int
  @currentIndex is the valid position into str
.parameterLength : ValidPositionstr -> Int
  @parameterLength is the length of the parameter str
count : (Char -> Bool) -> Positionstr -> 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
distance : Positionstr -> Positionstr -> 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
index : ValidPositionstr -> Char
  We can safely access the character at a valid position

Totality: total
init : (str : String) -> Positionstr
  Find the initial position inside the input string

Totality: total
mkPosition : (str : String) -> Int -> Positionstr
  Manufacture a position by checking it is strictly inside the string

Totality: total
mvPosition : ValidPositionstr -> Int -> Positionstr
  Move a position (note that we do not need access to the string here)

Totality: total
next : ValidPositionstr -> Positionstr
  Move from a valid position to the next position in the string

Totality: total
span : (Char -> Bool) -> Positionstr -> Positionstr
  @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
subString : Positionstr -> Positionstr -> String
  the substring of length `distance start end` that is contained between
start (inclusive) and end (exclusive).

Totality: total
uncons : ValidPositionstr -> (Char, Positionstr)
  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