String.Iterator #
This file contains String.Iterator, an outgoing API to be replaced by the iterator framework in
a future release.
An iterator over the characters (Unicode code points) in a String. Typically created by
String.iter.
This is a no-longer-supported legacy API that will be removed in a future release. You should use
String.ValidPos instead, which is similar, but safer. To iterate over a string s, start with
p : s.startValidPos, advance it using p.next, access the current character using p.get and
check if the position is at the end using p = s.endValidPos or p.IsAtEnd.
String iterators pair a string with a valid byte index. This allows efficient character-by-character processing of strings while avoiding the need to manually ensure that byte indices are used with the correct strings.
An iterator is valid if the position i is valid for the string s, meaning 0 ≤ i ≤ s.rawEndPos
and i lies on a UTF8 byte boundary. If i = s.rawEndPos, the iterator is at the end of the string.
Most operations on iterators return unspecified values if the iterator is not valid. The functions
in the String.Iterator API rule out the creation of invalid iterators, with two exceptions:
Iterator.next iteris invalid ifiteris already at the end of the string (iter.atEndistrue), andIterator.forward iter n/Iterator.nextn iter nis invalid ifnis strictly greater than the number of remaining characters.
- s : String
The string being iterated over.
- i : Pos.Raw
The current UTF-8 byte position in the string
s.This position is not guaranteed to be valid for the string. If the position is not valid, then the current character is
(default : Char), similar toString.geton an invalid position.
Instances For
Instances For
Equations
Creates an iterator at the beginning of the string.
This is a no-longer-supported legacy API that will be removed in a future release. You should use
String.ValidPos instead, which is similar, but safer. To iterate over a string s, start with
p : s.startValidPos, advance it using p.next, access the current character using p.get and
check if the position is at the end using p = s.endValidPos or p.IsAtEnd.
Equations
- String.Legacy.mkIterator s = { s := s, i := 0 }
Instances For
Creates an iterator at the beginning of the string.
This is a no-longer-supported legacy API that will be removed in a future release. You should use
String.ValidPos instead, which is similar, but safer. To iterate over a string s, start with
p : s.startValidPos, advance it using p.next, access the current character using p.get and
check if the position is at the end using p = s.endValidPos or p.IsAtEnd.
Equations
Instances For
The size of a string iterator is the number of bytes remaining.
Recursive functions that iterate towards the end of a string will typically decrease this measure.
Equations
- String.Legacy.instSizeOfIterator = { sizeOf := fun (i : String.Legacy.Iterator) => i.s.utf8ByteSize - i.i.byteIdx }
The string being iterated over.
Instances For
The current UTF-8 byte position in the string s.
This position is not guaranteed to be valid for the string. If the position is not valid, then the
current character is (default : Char), similar to String.get on an invalid position.
Instances For
Gets the character at the iterator's current position.
This is a no-longer-supported legacy API that will be removed in a future release. You should use
String.ValidPos instead, which is similar, but safer. To iterate over a string s, start with
p : s.startValidPos, advance it using p.next, access the current character using p.get and
check if the position is at the end using p = s.endValidPos or p.IsAtEnd.
A run-time bounds check is performed. Use String.Iterator.curr' to avoid redundant bounds checks.
If the position is invalid, returns (default : Char).
Equations
- { s := s, i := i }.curr = String.Pos.Raw.get s i
Instances For
Moves the iterator's position forward by one character, unconditionally.
This is a no-longer-supported legacy API that will be removed in a future release. You should use
String.ValidPos instead, which is similar, but safer. To iterate over a string s, start with
p : s.startValidPos, advance it using p.next, access the current character using p.get and
check if the position is at the end using p = s.endValidPos or p.IsAtEnd.
It is only valid to call this function if the iterator is not at the end of the string (i.e.
if Iterator.atEnd is false); otherwise, the resulting iterator will be invalid.
Instances For
Moves the iterator's position backward by one character, unconditionally.
The position is not changed if the iterator is at the beginning of the string.
Instances For
Gets the character at the iterator's current position.
The proof of it.hasNext ensures that there is, in fact, a character at the current position. This
function is faster that String.Iterator.curr due to avoiding a run-time bounds check.
Equations
- { s := s, i := i }.curr' h_2 = String.Pos.Raw.get' s i ⋯
Instances For
Moves the iterator's position forward by one character, unconditionally.
The proof of it.hasNext ensures that there is, in fact, a position that's one character forwards.
This function is faster that String.Iterator.next due to avoiding a run-time bounds check.
Instances For
Extracts the substring between the positions of two iterators. The first iterator's position is the start of the substring, and the second iterator's position is the end.
Returns the empty string if the iterators are for different strings, or if the position of the first iterator is past the position of the second iterator.
Equations
Instances For
Moves the iterator's position forward by the specified number of characters.
The resulting iterator is only valid if the number of characters to skip is less than or equal to the number of characters left in the iterator.
Instances For
The remaining characters in an iterator, as a string.
Equations
- { s := s, i := i }.remainingToString = String.Pos.Raw.extract s i s.rawEndPos
Instances For
Moves the iterator's position forward by the specified number of characters.
The resulting iterator is only valid if the number of characters to skip is less than or equal to the number of characters left in the iterator.
Instances For
Replaces the current character in the string.
Does nothing if the iterator is at the end of the string. If both the replacement character and the replaced character are 7-bit ASCII characters and the string is not shared, then it is updated in-place and not copied.
Instances For
Moves the iterator forward until the Boolean predicate p returns true for the iterator's current
character or until the end of the string is reached. Does nothing if the current character already
satisfies p.
Equations
Instances For
Iterates over a string, updating a state at each character using the provided function f, until
f returns none. Begins with the state init. Returns the state and character for which f
returns none.
Equations
Instances For
Returns an iterator into the underlying string, at the substring's starting position. The ending position is discarded, so the iterator alone cannot be used to determine whether its current position is within the original substring.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- instToStringIterator = { toString := fun (it : String.Legacy.Iterator) => it.remainingToString }