Equations
- String.instOfNatPos = { ofNat := { byteIdx := 0 } }
Equations
- String.instLT = { lt := fun (s₁ s₂ : String) => s₁.data < s₂.data }
Equations
- s₁.decLE s₂ = inferInstanceAs (Decidable ¬s₂ < s₁)
Pushes a character onto the end of a string.
The internal implementation uses dynamic arrays and will perform destructive updates if the string is not shared.
Example: "abc".push 'd' = "abcd"
Instances For
Appends two strings.
The internal implementation uses dynamic arrays and will perform destructive updates if the string is not shared.
Example: "abc".append "def" = "abcdef"
Instances For
Converts a string to a list of characters.
Even though the logical model of strings is as a structure that wraps a list of characters, this operation takes time and space linear in the length of the string, because the compiler uses an optimized representation as dynamic arrays.
Example: "abc".toList = ['a', 'b', 'c']
Equations
- s.toList = s.data
Instances For
Returns true if p
is a valid UTF-8 position in the string s
, meaning that p ≤ s.endPos
and p
lies on a UTF-8 character boundary. This has an O(1) implementation in the runtime.
Equations
- String.Pos.isValid s p = String.Pos.isValid.go p s.data 0
Instances For
Equations
- String.Pos.isValid.go p [] x✝ = decide (x✝ = p)
- String.Pos.isValid.go p (c :: cs) x✝ = if x✝ = p then true else String.Pos.isValid.go p cs (x✝ + c)
Instances For
Equations
- String.utf8GetAux [] x✝¹ x✝ = default
- String.utf8GetAux (c :: cs) x✝¹ x✝ = if x✝¹ = x✝ then c else String.utf8GetAux cs (x✝¹ + c) x✝
Instances For
Returns the character at position p
of a string. If p
is not a valid position,
returns (default : Char)
.
See utf8GetAux
for the reference implementation.
Examples:
Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8
character. For example,"L∃∀N".get ⟨2⟩ = (default : Char) = 'A'
.
Equations
- { data := s_1 }.get p = String.utf8GetAux s_1 0 p
Instances For
Equations
- String.utf8GetAux? [] x✝¹ x✝ = none
- String.utf8GetAux? (c :: cs) x✝¹ x✝ = if x✝¹ = x✝ then some c else String.utf8GetAux? cs (x✝¹ + c) x✝
Instances For
Returns the character at position p
. If p
is not a valid position, returns none
.
Examples:
Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8
character. For example, "L∃∀N".get? ⟨2⟩ = none
Equations
- { data := s }.get? x✝ = String.utf8GetAux? s 0 x✝
Instances For
Returns the character at position p
of a string. If p
is not a valid position,
returns (default : Char)
and produces a panic error message.
Examples:
Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example,
"L∃∀N".get! ⟨2⟩
panics.
Equations
- { data := s_1 }.get! p = String.utf8GetAux s_1 0 p
Instances For
Equations
- String.utf8SetAux c' [] x✝¹ x✝ = []
- String.utf8SetAux c' (c :: cs) x✝¹ x✝ = if x✝¹ = x✝ then c' :: cs else c :: String.utf8SetAux c' cs (x✝¹ + c) x✝
Instances For
Replaces the character at a specified position in a string with a new character. If the position is invalid, the string is returned unchanged.
If both the replacement character and the replaced character are ASCII characters and the string is not shared, destructive updates are used.
Examples:
Because '∃'
is a multi-byte character, the byte index 2
in L∃∀N
is an invalid position,
so "L∃∀N".set ⟨2⟩ 'X' = "L∃∀N"
.
Equations
- { data := s }.set x✝¹ x✝ = { data := String.utf8SetAux x✝ s 0 x✝¹ }
Instances For
Replaces the character at position p
in the string s
with the result of applying f
to that character.
If p
is an invalid position, the string is returned unchanged.
Examples:
abc.modify ⟨1⟩ Char.toUpper = "aBc"
abc.modify ⟨3⟩ Char.toUpper = "abc"
Equations
- s.modify i f = s.set i (f (s.get i))
Instances For
Returns the next position in a string after position p
. If p
is not a valid position or p = s.endPos
,
the result is unspecified.
Examples:
Given def abc := "abc"
and def lean := "L∃∀N"
,
Cases where the result is unspecified:
"abc".next ⟨3⟩
, since3 = s.endPos
"L∃∀N".next ⟨2⟩
, since2
points into the middle of a multi-byte UTF-8 character
Instances For
Equations
- String.utf8PrevAux [] x✝¹ x✝ = 0
- String.utf8PrevAux (c :: cs) x✝¹ x✝ = if x✝¹ + c = x✝ then x✝¹ else String.utf8PrevAux cs (x✝¹ + c) x✝
Instances For
Returns the position in a string before a specified position, p
. If p = ⟨0⟩
, returns 0
.
If p
is not a valid position, the result is unspecified.
Examples:
Given def abc := "abc"
and def lean := "L∃∀N"
,
abc.get (abc.endPos |> abc.prev) = 'c'
lean.get (lean.endPos |> lean.prev |> lean.prev |> lean.prev) = '∃'
"L∃∀N".prev ⟨3⟩
is unspecified, since byte 3 occurs in the middle of the multi-byte character'∃'
.
Equations
- { data := s }.prev x✝ = if x✝ = 0 then 0 else String.utf8PrevAux s 0 x✝
Instances For
Returns true
if a specified position is greater than or equal to the position which
points to the end of a string. Otherwise, returns false
.
Examples:
Given def abc := "abc"
and def lean := "L∃∀N"
,
(0 |> abc.next |> abc.next |> abc.atEnd) = false
(0 |> abc.next |> abc.next |> abc.next |> abc.next |> abc.atEnd) = true
(0 |> lean.next |> lean.next |> lean.next |> lean.next |> lean.atEnd) = true
Because "L∃∀N"
contains multi-byte characters, lean.next (lean.next 0)
is not equal to abc.next (abc.next 0)
.
Instances For
Returns the character at position p
of a string.
If p
is not a valid position, returns (default : Char)
.
Requires evidence, h
, that p
is within bounds
instead of performing a runtime bounds check as in get
.
Examples:
"abc".get' 0 (by decide) = 'a'
let lean := "L∃∀N"; lean.get' (0 |> lean.next |> lean.next) (by decide) = '∀'
A typical pattern combines get'
with a dependent if-else expression
to avoid the overhead of an additional bounds check. For example:
def getInBounds? (s : String) (p : String.Pos) : Option Char :=
if h : s.atEnd p then none else some (s.get' p h)
Even with evidence of ¬ s.atEnd p
,
p
may be invalid if a byte index points into the middle of a multi-byte UTF-8 character.
For example, "L∃∀N".get' ⟨2⟩ (by decide) = (default : Char)
.
Equations
- { data := s_2 }.get' p h_2 = String.utf8GetAux s_2 0 p
Instances For
Returns the next position in a string after position p
.
If p
is not a valid position, the result is unspecified.
Requires evidence, h
, that p
is within bounds
instead of performing a runtime bounds check as in next
.
Examples:
A typical pattern combines next'
with a dependent if-else expression
to avoid the overhead of an additional bounds check. For example:
def next? (s: String) (p : String.Pos) : Option Char :=
if h : s.atEnd p then none else s.get (s.next' p h)
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Returns the first position where the two strings differ.
Equations
- a.firstDiffPos b = String.firstDiffPos.loop a b (a.endPos.min b.endPos) 0
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- { data := s }.extract x✝¹ x✝ = if x✝¹.byteIdx ≥ x✝.byteIdx then "" else { data := String.extract.go₁ s 0 x✝¹ x✝ }
Instances For
Equations
- String.extract.go₁ [] x✝² x✝¹ x✝ = []
- String.extract.go₁ (c :: cs) x✝² x✝¹ x✝ = if x✝² = x✝¹ then String.extract.go₂ (c :: cs) x✝² x✝ else String.extract.go₁ cs (x✝² + c) x✝¹ x✝
Instances For
Equations
- String.extract.go₂ [] x✝¹ x✝ = []
- String.extract.go₂ (c :: cs) x✝¹ x✝ = if x✝¹ = x✝ then [] else c :: String.extract.go₂ cs (x✝¹ + c) x✝
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Auxiliary for splitOn
. Preconditions:
It represents the state where we have currently parsed some split parts into r
(in reverse order),
b
is the beginning of the string / the end of the previous match of sep
, and the first j
bytes
of sep
match the bytes i-j .. i
of s
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Splits a string s
on occurrences of the separator sep
. When sep
is empty, it returns [s]
;
when sep
occurs in overlapping patterns, the first match is taken. There will always be exactly
n+1
elements in the returned list if there were n
nonoverlapping matches of sep
in the string.
The default separator is " "
. The separators are not included in the returned substrings.
"here is some text ".splitOn = ["here", "is", "some", "text", ""]
"here is some text ".splitOn "some" = ["here is ", " text "]
"here is some text ".splitOn "" = ["here is some text "]
"ababacabac".splitOn "aba" = ["", "bac", "c"]
Instances For
Equations
- String.instInhabited = { default := "" }
Equations
- String.instAppend = { append := String.append }
Equations
- s.intercalate [] = ""
- s.intercalate (a :: as) = String.intercalate.go a s as
Instances For
Equations
- String.intercalate.go acc s (a :: as) = String.intercalate.go (acc ++ s ++ a) s as
- String.intercalate.go acc s [] = acc
Instances For
Iterator over the characters (Char
) of a String
.
Typically created by s.iter
, where s
is a String
.
An iterator is valid if the position i
is valid for the string s
, meaning 0 ≤ i ≤ s.endPos
and i
lies on a UTF8 byte boundary. If i = s.endPos
, the iterator is at the end of the string.
Most operations on iterators return arbitrary values if the iterator is not valid. The functions in
the String.Iterator
API should rule out the creation of invalid iterators, with two exceptions:
Iterator.next iter
is invalid ifiter
is already at the end of the string (iter.atEnd
istrue
), andIterator.forward iter n
/Iterator.nextn iter n
is invalid ifn
is strictly greater than the number of remaining characters.
- s : String
The string the iterator is for.
- i : String.Pos
The current position.
This position is not necessarily valid for the string, for instance if one keeps calling
Iterator.next
whenIterator.atEnd
is true. If the position is not valid, then the current character is(default : Char)
, similar toString.get
on an invalid position.
Instances For
Equations
- String.instInhabitedIterator = { default := { s := default, i := default } }
Creates an iterator at the beginning of a string.
Equations
- s.mkIterator = { s := s, i := 0 }
Instances For
Creates an iterator at the beginning of a string.
Equations
Instances For
The size of a string iterator is the number of bytes remaining.
Equations
- String.instSizeOfIterator = { sizeOf := fun (i : String.Iterator) => i.s.utf8ByteSize - i.i.byteIdx }
The string the iterator is for.
Equations
Instances For
Number of bytes remaining in the iterator.
Instances For
The current position.
This position is not necessarily valid for the string, for instance if one keeps calling
Iterator.next
when Iterator.atEnd
is true. If the position is not valid, then the
current character is (default : Char)
, similar to String.get
on an invalid position.
Equations
Instances For
The character at the current position.
On an invalid position, returns (default : Char)
.
Equations
- { s := s, i := i }.curr = s.get i
Instances For
Moves the iterator's position forward by one character, unconditionally.
It is only valid to call this function if the iterator is not at the end of the string, i.e.
Iterator.atEnd
is false
; otherwise, the resulting iterator will be invalid.
Equations
- { s := s, i := i }.next = { s := s, i := s.next i }
Instances For
Decreases the iterator's position.
If the position is zero, this function is the identity.
Equations
- { s := s, i := i }.prev = { s := s, i := s.prev i }
Instances For
True if the iterator is past the string's last character.
Instances For
True if the iterator is not past the string's last character.
Instances For
True if the position is not zero.
Instances For
Replaces the current character in the string.
Does nothing if the iterator is at the end of the string. If the iterator contains the only reference to its string, this function will mutate the string in-place instead of allocating a new one.
Equations
- { s := s, i := i }.setCurr x✝ = { s := s.set i x✝, i := i }
Instances For
Extracts the substring between the positions of two iterators.
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 several characters forward.
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 = s.extract i s.endPos
Instances For
Moves the iterator's position several characters forward.
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
Moves the iterator's position several characters back.
If asked to go back more characters than available, stops at the beginning of the string.
Instances For
Equations
- String.foldlAux f s stopPos i a = if h : i < stopPos then let_fun this := ⋯; String.foldlAux f s stopPos (s.next i) (f a (s.get i)) else a
Instances For
Equations
- String.foldrAux f a s i begPos = if h : begPos < i then let_fun this := ⋯; let i := s.prev i; let a := f (s.get i) a; String.foldrAux f a s i begPos else a
Instances For
Equations
Instances For
Equations
- String.mapAux f i s = if h : s.atEnd i = true then s else let c := f (s.get i); let_fun this := ⋯; let s := s.set i c; String.mapAux f (s.next i) s
Instances For
Return true
iff the substring of byte size sz
starting at position off1
in s1
is equal to that starting at off2
in s2.
.
False if either substring of that byte size does not exist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Replace all occurrences of pattern
in s
with replacement
.
Equations
- s.replace pattern replacement = if h : pattern.endPos.byteIdx = 0 then s else let_fun hPatt := ⋯; String.replace.loop s pattern replacement hPatt "" 0 0
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- { str := s, startPos := b, stopPos := e }.toIterator = { s := s, i := b }
Instances For
Return the codepoint at the given offset into the substring.
Instances For
Given an offset of a codepoint into the substring, return the offset there of the next codepoint.
Equations
Instances For
Given an offset of a codepoint into the substring, return the offset there of the previous codepoint.
Equations
Instances For
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Substring.foldl f init { str := s_1, startPos := b, stopPos := e } = String.foldlAux f s_1 e b init
Instances For
Equations
- Substring.foldr f init { str := s_1, startPos := b, stopPos := e } = String.foldrAux f init s_1 e b
Instances For
Equations
- Substring.takeWhileAux s stopPos p i = if h : i < stopPos then if p (s.get i) = true then let_fun this := ⋯; Substring.takeWhileAux s stopPos p (s.next i) else i else i
Instances For
Equations
- { str := s, startPos := b, stopPos := e }.takeWhile x✝ = { str := s, startPos := b, stopPos := Substring.takeWhileAux s e x✝ b }
Instances For
Equations
- { str := s, startPos := b, stopPos := e }.dropWhile x✝ = { str := s, startPos := Substring.takeWhileAux s e x✝ b, stopPos := e }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- { str := s, startPos := b, stopPos := e }.takeRightWhile x✝ = { str := s, startPos := Substring.takeRightWhileAux s b x✝ e, stopPos := e }
Instances For
Equations
- { str := s, startPos := b, stopPos := e }.dropRightWhile x✝ = { str := s, startPos := b, stopPos := Substring.takeRightWhileAux s b x✝ e }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns the longest common prefix of two substrings.
The returned substring will use the same underlying string as s
.
Equations
- s.commonPrefix t = { str := s.str, startPos := s.startPos, stopPos := Substring.commonPrefix.loop s t s.startPos t.startPos }
Instances For
Returns the ending position of the common prefix, working up from spos, tpos
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns the longest common suffix of two substrings.
The returned substring will use the same underlying string as s
.
Equations
- s.commonSuffix t = { str := s.str, startPos := Substring.commonSuffix.loop s t s.stopPos t.stopPos, stopPos := s.stopPos }
Instances For
Returns the starting position of the common prefix, working down from spos, tpos
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
s.stripPrefix pre
will remove pre
from the beginning of s
if it occurs there,
or otherwise return s
.
Equations
- s.stripPrefix pre = (Option.map Substring.toString (s.dropPrefix? pre)).getD s
Instances For
s.stripSuffix suff
will remove suff
from the end of s
if it occurs there,
or otherwise return s
.
Equations
- s.stripSuffix suff = (Option.map Substring.toString (s.dropSuffix? suff)).getD s