12.8. 文字列(Strings)🔗

文字列は Unicode テキストを表現しています。文字列は Lean で特別にサポートされています:

  • 文字のリストという観点から動作を指定する 論理モデル を持っており、文字列に対する各操作の意味を指定します。

  • コンパイルされたコードにおいて文字列を UTF-8 としてエンコードするバイトの packed array として最適化されたランタイム表現を持っており、Lean ランタイムは特別に文字列操作を最適化します。

  • 文字列を書くための 文字列リテラルの構文 があります。

文字列が内部的に UTF-8 エンコードされたバイト配列として表現されていることは API で確認できます:

  • 文字列から特定の文字を射影する操作はありません(仮にあった場合パフォーマンスの罠になりえます)。 の代わりに をループ内で使ってください。

  • 文字列は によってインデックス付けされ、内部的には 文字数 ではなく バイト数 を記録するため、一定の時間がかかります。0 は別として、これらは直接構成されるのではなく、 をつかって更新されます。

12.8.1. 論理モデル(Logical Model)

🔗structure
String : Type

is the type of (UTF-8 encoded) strings.

The compiler overrides the data representation of this type to a byte sequence, and both and are cached and O(1).

Constructor

Pack a into a . This function is overridden by the compiler and is O(n) in the length of the list.

Fields

 :  

Unpack into a . This function is overridden by the compiler and is O(n) in the length of the list.

Lean における文字列の論理モデルは、文字のリストである1つのフィールドを含む構造体です。これは低レベルで文字列処理関数のプロパティを指定したり証明したりするときに便利です。

12.8.2. ランタイム表現(Run-Time Representation)🔗

Memory layout of strings

Memory layout of strings

文字列はバイトの 動的配列 として表現され、UTF-8 でエンコードされます。オブジェクトヘッダの後、文字列は以下を含みます:

バイト数

現在有効な文字列データを含むバイト数

容量

現在文字列に割り当てられているバイト数

長さ

エンコードされた文字列の長さ。UTF-8 のマルチバイト文字のため、バイト数よりも短くなる可能性があります。

データ

ヌル文字で終端された文字列内の実際の文字データ

Lean ランタイムの多くの文字列関数は、おぷじぇくとヘッダの参照カウントを参照することで引数に排他的アクセスがあるかどうかをチェックします。もしアクセスがあり、かつ文字列の容量が十分であれば、新しいメモリを確保するのではなく、既存の文字列を変更することができます。そうでない場合は新しい文字列を割り当てなければなりません。

12.8.2.1. パフォーマンスについての注記(Performance Notes)🔗

一見普通のコンストラクタと射影に見えますが、 文字列の長さに比例した時間 がかかります。これは文字のリストとバイトの packed array の間の変換を実装しなければならないためで、各文字を必ず訪問しなければなりません。

12.8.3. 構文(Syntax)🔗

Lean には3種類の文字列リテラルがあります:通常の文字列リテラル・補間文字列リテラル・生文字列リテラル

12.8.3.1. 文字列リテラル(String Literals)🔗

文字列リテラルはダブルクォート文字 " で開始・終了します。 これらの文字の間には、改行文字を(文字通り)含む他の任意の文字を含めることができます(ただし、Lean ソースファイル内のすべての改行文字はファイルのエンコーディングやプラットフォームに関係なく '\n' として解釈されます)。文字列リテラルにかけない特殊文字はバックスラッシュでエスケープすることができるため、 "\"Quotes\"" は二重引用符で開始・終了する文字列リテラルです。以下の形式のエスケープシーケンスが利用できます:

\r\n\t\\\"\'

これらのエスケープシーケンスは通常の意味を持ち、それぞれ CRLF・タブ・バックスラッシュ・二重引用符・引用符に対応します。

\xNN

NN が2桁の16進数である時、このエスケープは2桁の16進数で示される Unicode コードポイントを持つ文字を表します。

\uNNNN

NN が2桁の16進数である時、このエスケープは4桁の16進数コードで示される Unicode コードポイントを持つ文字を表します。

文字列リテラルは ギャップ (gap)を含むことができます。ギャップはエスケープされた開業で示され、エスケープされたバックスラッシュと改行の間には文字が介在しません。この場合、リテラルで示される文字列には、改行と次の行の先頭の空白がすべて含まれません。文字列のギャップは空白のみを含む行の前にあってはなりません。

:= := : = :=

ギャップに続く行が空の場合、その文字列は拒否されます:

def str3 := "String with \             a gap"

パーサは以下のエラーを返します:

<example>:2:0: unexpected additional newline in string gap

12.8.3.2. 補間文字列(Interpolated Strings)🔗

文字列の前に s! を置くと、 補間文字列 (interpolated string)として処理されます。この文字列内の {} で囲まれた領域がパースされ、Lean の式として解釈されます。補間文字列は、補間の前の文字列・式(それを囲む の呼び出しが追加されたもの)・補間後の文字列が連結されたものとして解釈されます。

例えば:

: "1 + 1 = {1 + 1}\n" = ++ (1 + 1) ++ :=

リテラルの前に m! を置くと、 のインスタンスとなります。これはコンパイラの内部からユーザ向けに使用されるメッセージのデータ構造です。

12.8.3.3. 生文字列リテラル🔗

生文字列リテラル (raw string literal)では、エスケープシーケンスやギャップはなく、各文字はそれ自身を正確に表します。生文字列リテラルは r で始まり、0個以上のハッシュ文字(#)と二重引用符 " が続きます。文字列リテラルは 同じ数 のハッシュ文字が続く二重引用符で補完されます。例えば、特定の文字をダブルエスケープする必要を避けるために使用することができます:

: = :=

この #eval は以下を出力します:

"Write backslash in a string using '\\\\\\\\'"

ハッシュ記号を含めると、文字列にエスケープされていない引用符を含めることができます。

: = :=

十分な数のハッシュ記号を追加することで、どんな生リテラルでも文字通りに書くことができます:

: = :=

12.8.4. API リファレンス(API Reference)🔗

12.8.4.1. 構成(Constructing)🔗

🔗def
String.singleton (c : ) : 
🔗def
String.append : 

Appends two strings.

The internal implementation uses dynamic arrays and will perform destructive updates if the string is not shared.

Example: . =

🔗def
String.join (l :  ) : 
🔗def
String.intercalate (s : )
    :  

12.8.4.2. 変換(Conversions)🔗

🔗def
String.toList (s : ) :  

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: . = ['a', 'b', 'c']

🔗def
String.isNat (s : ) : 
🔗def
String.toNat? (s : ) :  
🔗def
String.toNat! (s : ) : 

Interpret the string as the decimal representation of a natural number.

Panics if the string is not a string of digits.

🔗def
String.isInt (s : ) : 
🔗def
String.toInt? (s : ) :  
🔗def
String.toInt! (s : ) : 
🔗def
String.toFormat (s : ) : 

12.8.4.3. プロパティ(Properties)🔗

🔗def
String.isEmpty (s : ) : 
🔗def
String.length : 

Returns the length of a string in Unicode code points.

Examples:

12.8.4.4. 位置(Positions)🔗

🔗structure
String.Pos : Type

A byte position in a . Internally, s are UTF-8 encoded. Codepoint positions (counting the Unicode codepoints rather than bytes) are represented by plain s instead. Indexing a by a byte position is constant-time, while codepoint positions need to be translated internally to byte positions in linear-time.

A byte position p is valid for a string s if 0 p s.endPos and p lies on a UTF8 byte boundary.

Constructor

Fields

 : 

Get the underlying byte index of a

🔗def
String.Pos.isValid (s : ) (p : )
    : 

Returns true if is a valid UTF-8 position in the string , meaning that . and lies on a UTF-8 character boundary. This has an O(1) implementation in the runtime.

🔗def
String.atEnd : 

Returns if a specified position is greater than or equal to the position which points to the end of a string. Otherwise, returns .

Examples: Given abc := and lean := ,

  • (0 |> abc.next |> abc.next |> abc.atEnd) =

  • (0 |> abc.next |> abc.next |> abc.next |> abc.next |> abc.atEnd) =

  • (0 |> lean.next |> lean.next |> lean.next |> lean.next |> .atEnd) =

Because contains multi-byte characters, .next (lean.next 0) is not equal to abc.next (abc.next 0).

🔗def
String.endPos (s : ) : 

A pointing at the end of this string.

🔗def
String.next (s : ) (p : )
    : 

Returns the next position in a string after position . If is not a valid position or = ., the result is unspecified.

Examples: Given abc := and lean := ,

  • abc.get (0 |> abc.next) = 'b'

  • .get (0 |> lean.next |> lean.next) = '∀'

Cases where the result is unspecified:

  • . 3, since 3 = .

  • . 2, since 2 points into the middle of a multi-byte UTF-8 character

🔗def
String.next' (s : ) (p : )
    (h : .atEnd ) : 

Returns the next position in a string after position . If is not a valid position, the result is unspecified.

Requires evidence, , that is within bounds instead of performing a runtime bounds check as in .

Examples:

A typical pattern combines next' with a dependent if-else expression to avoid the overhead of an additional bounds check. For example:

(: ) ( : ) : := : . . (. )
🔗def
String.nextWhile (s : ) (p : )
    (i : ) : 
🔗def
String.nextUntil (s : ) (p : )
    (i : ) : 
🔗def
String.prev : 

Returns the position in a string before a specified position, . If = 0, returns 0. If is not a valid position, the result is unspecified.

Examples: Given abc := and lean := ,

  • abc.get (abc.endPos |> abc.prev) = 'c'

  • .get (lean.endPos |> lean.prev |> lean.prev |> lean.prev) = '∃'

  • . 3 is unspecified, since byte 3 occurs in the middle of the multi-byte character '∃'.

🔗def
String.Pos.min (p₁ p₂ : ) : 

12.8.4.5. 検索と変更(Lookups and Modifications)🔗

🔗def
String.get (s : ) (p : ) : 

Returns the character at position of a string. If is not a valid position, returns ( : ).

See utf8GetAux for the reference implementation.

Examples:

  • . 1 = 'b'

  • .get 3 = (default : Char) = 'A'

Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example,.get 2 = (default : Char) = 'A'.

🔗def
String.get? :  

Returns the character at position p. If p is not a valid position, returns .

Examples:

Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example, . 2 =

🔗def
String.get! (s : ) (p : ) : 

Returns the character at position of a string. If is not a valid position, returns ( : ) and produces a panic error message.

Examples:

  • . 1 = 'b'

  • . 3 panics

Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example, . 2 panics.

🔗def
String.get' (s : ) (p : )
    (h : .atEnd ) : 

Returns the character at position of a string. If is not a valid position, returns ( : ).

Requires evidence, , that is within bounds instead of performing a runtime bounds check as in .

Examples:

A typical pattern combines get' with a dependent if-else expression to avoid the overhead of an additional bounds check. For example:

( : ) ( : ) : := : . (. )

Even with evidence of ¬ . , may be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example, . 2 ( ) = ( : ).

🔗def
String.extract
    : 
🔗def
String.take (s : ) (n : ) : 
🔗def
String.takeWhile (s : ) (p : )
    : 
🔗def
String.takeRight (s : ) (n : ) : 
🔗def
String.takeRightWhile (s : )
    (p : ) : 
🔗def
String.drop (s : ) (n : ) : 
🔗def
String.dropWhile (s : ) (p : )
    : 
🔗def
String.dropRight (s : ) (n : ) : 
🔗def
String.dropRightWhile (s : )
    (p : ) : 
🔗def
String.trim (s : ) : 
🔗def
String.trimLeft (s : ) : 
🔗def
String.trimRight (s : ) : 
🔗def
String.removeLeadingSpaces (s : ) : 
🔗def
String.set : 

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:

  • . 1 'B' =

  • . 3 'D' =

  • . 4 'X' =

Because '∃' is a multi-byte character, the byte index 2 in LN is an invalid position, so . 2 'X' = .

🔗def
String.modify (s : ) (i : )
    (f : ) : 

Replaces the character at position p in the string with the result of applying to that character. If p is an invalid position, the string is returned unchanged.

Examples:

  • abc.modify 1 Char.toUpper =

  • abc.modify 3 Char.toUpper =

🔗def
String.front (s : ) : 

Returns the first character in . If = , returns ( : ).

Examples:

🔗def
String.back (s : ) : 

Returns the last character in . If = , returns ( : ).

Examples:

🔗def
String.posOf (s : ) (c : )
    : 

Returns the position of the first occurrence of a character, , in . If does not contain , returns ..

Examples:

  • . 'a' = 0

  • . 'z' = 4

  • . '∀' = 4

🔗def
String.revPosOf (s : ) (c : )
    :  

Returns the position of the last occurrence of a character, , in . If does not contain , returns .

Examples:

🔗def
String.contains (s : ) (c : ) : 
🔗def
String.offsetOfPos (s : )
    (pos : ) : 
🔗def
String.replace (s pattern replacement : )
    : 

Replace all occurrences of in with .

🔗def
String.findLineStart (s : )
    (pos : ) : 

Return the beginning of the line that contains character .

🔗def
String.find (s : ) (p : )
    : 
🔗def
String.revFind (s : ) (p : )
    :  

12.8.4.6. 畳み込みと集約(Folds and Aggregation)🔗

🔗def
String.map (f : ) (s : )
    : 
🔗def
String.foldl.{u} {α : Type u} (f : )
    (init : ) (s : ) : 
🔗def
String.foldr.{u} {α : Type u} (f : )
    (init : ) (s : ) : 
🔗def
String.all (s : ) (p : ) : 
🔗def
String.any (s : ) (p : ) : 

12.8.4.7. 比較(Comparisons)🔗

🔗def
String.le (a b : ) : Prop
🔗def
String.firstDiffPos (a b : ) : 

Returns the first position where the two strings differ.

🔗def
String.substrEq (s1 : )
    (off1 : ) (s2 : )
    (off2 : ) (sz : ) : 

Return iff the substring of byte size starting at position in is equal to that starting at in .. False if either substring of that byte size does not exist.

🔗def
String.isPrefixOf (p s : ) : 

Return true iff is a prefix of

🔗def
String.startsWith (s pre : ) : 
🔗def
String.endsWith (s post : ) : 
🔗def
String.decEq (s₁ s₂ : )
    :  ()

Decides equality on . This function is overridden with a native implementation.

🔗opaque
String.hash (s : ) : 

An opaque string hash function.

12.8.4.8. 操作(Manipulation)🔗

🔗def
String.split (s : ) (p : )
    :  
🔗def
 (s : )
  (sep :  := ) :  

Splits a string on occurrences of the separator . When is empty, it returns []; when occurs in overlapping patterns, the first match is taken. There will always be exactly +1 elements in the returned list if there were nonoverlapping matches of 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"]
🔗def
String.push : 

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: . 'd' =

🔗def
String.pushn (s : ) (c : ) (n : )
    : 
🔗def
String.capitalize (s : ) : 
🔗def
String.decapitalize (s : ) : 
🔗def
String.toUpper (s : ) : 
🔗def
String.toLower (s : ) : 

12.8.4.9. イテレータ(Iterators)🔗

基本的に、 は文字列と文字列内の有効な位置のペアです。イテレータは現在の文字を取得する関数( )・現在の文字を置き換える関数( )・イテレータが左または右に移動できるかどうかチェックする関数(それぞれ )・イテレータの移動(それぞれ )です。クライアントは文字列の先頭または末尾に到達したかどうかをチェックする責任があります;それ以外の場合、イテレータはその位置が常に文字を指すようにします。

🔗structure
String.Iterator : Type

Iterator over the characters () of a .

Typically created by s.iter, where s is a .

An iterator is valid if the position is valid for the string s, meaning 0 i s.endPos and lies on a UTF8 byte boundary. If = 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 API should rule out the creation of invalid iterators, with two exceptions:

  • Iterator.next iter is invalid if iter is already at the end of the string (iter.atEnd is ), and

  • Iterator.forward iter n/Iterator.nextn iter n is invalid if n is strictly greater than the number of remaining characters.

Constructor

Fields

 : 

The string the iterator is 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 ( : ), similar to on an invalid position.

🔗def
String.iter (s : ) : 

Creates an iterator at the beginning of a string.

🔗def
String.mkIterator (s : ) : 

Creates an iterator at the beginning of a string.

🔗def
String.Iterator.curr : 

The character at the current position.

On an invalid position, returns ( : ).

🔗def
String.Iterator.hasNext : 

True if the iterator is not past the string's last character.

🔗def
String.Iterator.next
    : 

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 ; otherwise, the resulting iterator will be invalid.

🔗def
String.Iterator.forward
    : 

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.

🔗def
String.Iterator.nextn
    : 

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.

🔗def
String.Iterator.hasPrev : 

True if the position is not zero.

🔗def
String.Iterator.prev
    : 

Decreases the iterator's position.

If the position is zero, this function is the identity.

🔗def
String.Iterator.prevn
    : 

Moves the iterator's position several characters back.

If asked to go back more characters than available, stops at the beginning of the string.

🔗def
String.Iterator.atEnd : 

True if the iterator is past the string's last character.

🔗def
String.Iterator.toEnd
    : 

Moves the iterator's position to the end of the string.

Note that i.toEnd.atEnd is always .

🔗def
String.Iterator.setCurr
    : 

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.

🔗def
String.Iterator.extract
    : 

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.

🔗def
String.Iterator.remainingToString
    : 

The remaining characters in an iterator, as a string.

🔗def
String.Iterator.remainingBytes
    : 

Number of bytes remaining in the iterator.

🔗def
String.Iterator.pos (self : )
    : 

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 ( : ), similar to on an invalid position.

12.8.4.10. 部分文字列(Substrings)🔗

🔗def
String.toSubstring (s : ) : 

Convert a into a denoting the entire string.

🔗def
String.toSubstring' (s : ) : 

without [inline] annotation.

12.8.4.11. 証明自動化(Proof Automation)🔗

🔗def
String.reduceGT : 
🔗def
String.reduceGE : 
🔗def
String.reduceBinPred (declName : )
    (arity : ) (op : )
    (e : )
    :  
🔗def
String.reduceLT : 
🔗def
String.reduceLE : 
🔗def
String.reduceBEq : 
🔗def
String.reduceEq : 
🔗def
String.reduceAppend : 
🔗def
String.reduceMk : 
🔗def
String.reduceBoolPred (declName : )
    (arity : ) (op : )
    (e : )
    :  
🔗def
String.reduceBNe : 
🔗def
String.reduceNe : 

12.8.4.12. メタプログラミング(Metaprogramming)🔗

🔗def
String.toName (s : ) : 

Converts a to a hierarchical Name after splitting it at the dots.

. is the name a.b, not «a.b». For the latter, use Name.mkSimple.

🔗def
String.toFileMap (s : ) : 
🔗def
String.quote (s : ) : 
🔗def
String.fromExpr? (e : )
    :  ( )

12.8.4.13. エンコード(Encodings)🔗

🔗def
String.utf16PosToCodepointPos (s : )
    (pos : ) : 
🔗def
String.utf16PosToCodepointPosFrom (s : )
    (utf16pos : ) (off : ) : 

Computes the position of the Unicode codepoint at UTF-16 offset in the substring of starting at UTF-8 offset .

🔗def
String.codepointPosToUtf16Pos (s : )
    (pos : ) : 
🔗def
String.codepointPosToUtf16PosFrom (s : )
    (n : ) (off : ) : 

Computes the UTF-16 offset of the -th Unicode codepoint in the substring of starting at UTF-8 offset . Yes, this is actually useful.

🔗def
String.getUtf8Byte (s : ) (n : )
    (h : .utf8ByteSize) : 

Accesses a byte in the UTF-8 encoding of the . O(1)

🔗def
String.utf8ByteSize : 

The UTF-8 byte length of this string. This is overridden by the compiler to be cached and O(1).

🔗def
String.utf8EncodeChar (c : ) :  
🔗def
String.utf8DecodeChar? (a : ) (i : )
    :  
🔗def
String.fromUTF8 (a : )
    (h :  ) : 

Converts a UTF-8 encoded string to .

🔗def
String.fromUTF8? (a : ) :  

Converts a UTF-8 encoded string to , or returns if is not properly UTF-8 encoded.

🔗def
String.fromUTF8! (a : ) : 

Converts a UTF-8 encoded string to , or panics if is not properly UTF-8 encoded.

🔗def
String.toUTF8 (a : ) : 

Converts the given to a UTF-8 encoded byte array.

🔗def
String.validateUTF8 (a : ) : 

Returns true if the given byte array consists of valid UTF-8.

🔗def
String.utf16Length (s : ) : 
🔗def
String.codepointPosToUtf8PosFrom (s : )
    : 

Starting at utf8pos, finds the UTF-8 offset of the p-th codepoint.

🔗def
String.crlfToLf (text : ) : 

Replaces each \r\n with \n to normalize line endings, but does not validate that there are no isolated \r characters. It is an optimized version of .

12.8.5. FFI🔗

🔗def
String.csize (c : ) : 
FFI type
typedef struct {
    lean_object m_header;
    /* byte length including '\0' terminator */
    size_t      m_size;
    size_t      m_capacity;
    /* UTF8 length */
    size_t      m_length;
    char        m_data[0];
} lean_string_object;

C での文字列の表現。詳細は のランタイムについての説明 を参照してください。

FFI function
bool lean_is_string(lean_object * o)

o が文字列であれば true を、そうでなければ false を返します。

FFI function
lean_string_object * lean_to_string(lean_object * o)

o が本当に文字列であることのランタイムチェックの実行。o が文字列でない場合は失敗を主張します。

Planned Content

Tracked at issue #158