Idris2Doc : Data.String.Position


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