- Position : String -> Type
A position is either a ValidPosition or the end of the string
- 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
- MkValidPosition : Int -> Int -> ValidPosition str
- .currentIndex : ValidPosition str -> Int
@currentIndex is the valid position into str
- .parameterLength : ValidPosition str -> Int
@parameterLength is the length of the parameter str
- 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.
- 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.
- index : ValidPosition str -> Char
We can safely access the character at a valid position
- init : (str : String) -> Position str
Find the initial position inside the input string
- mkPosition : (str : String) -> Int -> Position str
Manufacture a position by checking it is strictly inside the string
- mvPosition : ValidPosition str -> Int -> Position str
Move a position (note that we do not need access to the string here)
- next : ValidPosition str -> Position str
Move from a valid position to the next position in the string
- 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)
- subString : Position str -> Position str -> String
the substring of length `distance start end` that is contained between
start (inclusive) and end (exclusive).
- 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