From b8592b64ca1af651133570112282c23ce2e67405 Mon Sep 17 00:00:00 2001 From: s-taiga <56785231+s-taiga@users.noreply.github.com> Date: Sat, 23 Nov 2024 16:57:00 +0900 Subject: [PATCH] =?UTF-8?q?BasicTypes=E7=BF=BB=E8=A8=B3=20(#15)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 翻訳開始 * 翻訳完了 --- GLOSSARY.md | 3 + Manual/BasicTypes.lean | 43 +++++++ Manual/BasicTypes/Nat.lean | 148 +++++++++++++++++++++++++ Manual/BasicTypes/String.lean | 146 +++++++++++++++++++++++- Manual/BasicTypes/String/FFI.lean | 21 +++- Manual/BasicTypes/String/Literals.lean | 104 +++++++++++++++++ Manual/BasicTypes/String/Logical.lean | 8 ++ 7 files changed, 469 insertions(+), 4 deletions(-) diff --git a/GLOSSARY.md b/GLOSSARY.md index 2718662..feac9d0 100644 --- a/GLOSSARY.md +++ b/GLOSSARY.md @@ -111,6 +111,7 @@ | identifier component | 識別子要素 | | | identifier continuation character | 識別子継続文字 | | | identity function | 恒等関数 | | +| immediate value | 即値 | | | imperative | 命令型 | | | implicit parameter | 暗黙のパラメータ | | | inaccessible | （仮定のアクセス可否の文脈で）アクセス不能 | | @@ -134,6 +135,7 @@ | interface | インタフェース | | | interleave | 交互に実行する | | | intermediate representation | 中間表現 | | +| interpolate | 補間 | | | invariant | 不変量 | | | kernel | カーネル | | | keyword | キーワード | | @@ -289,6 +291,7 @@ | choice node | | | cumulative | | | impredicativity, predicativity | | +| no confusion | | | packed array | System Verilogという言語にこの名前の文法要素がある？ | | strict positively, negatively | 自己言及される定義の分類、定訳は無い模様 | | prelude | | diff --git a/Manual/BasicTypes.lean b/Manual/BasicTypes.lean index 8f3d202..b75a7f4 100644 --- a/Manual/BasicTypes.lean +++ b/Manual/BasicTypes.lean @@ -17,12 +17,20 @@ open Verso.Genre Manual set_option pp.rawOnError true +/- #doc (Manual) "Basic Types" => +-/ +#doc (Manual) "基本的な型（Basic Types）" => +:::comment Lean includes a number of built-in datatypes that are specially supported by the compiler. Some, such as {lean}`Nat`, additionally have special support in the kernel. Other types don't have special compiler support _per se_, but rely in important ways on the internal representation of types for performance reasons. +::: + +Lean にはコンパイラが特別にサポートする組み込みのデータ型が多数あります。 {lean}`Nat` のように、カーネルで特別にサポートされているものもあります。その他の型はコンパイラからの特別なサポート _自体_ はありませんが、パフォーマンス上の理由から型の内部表現に依存しています。 + {include 0 Manual.BasicTypes.Nat} # Integers @@ -54,25 +62,60 @@ Other types don't have special compiler support _per se_, but rely in important * Relationship between IEEE floats and decidable equality ::: +:::comment # Characters +::: + +# 文字（Characters） + {docstring Char} +:::comment ## Syntax +::: + +## 構文（Syntax） + +:::comment ## Logical Model +::: + +## 論理モデル（Logical Model） + +:::comment ## Run-Time Representation +::: + +## ランタイム表現（Run-Time Representation） + +:::comment In monomorphic contexts, characters are represented as 32-bit immediate values. In other words, a field of a datatype or structure of type `Char` does not require indirection to access. In polymorphic contexts, characters are boxed. +::: + +モノ射なコンテキストでは、文字は32ビットの即値として表現されます。言い換えると、`Char` 型のデータ型や構造体のフィールドにアクセスする際にインダイレクトは必要ありません。多相なコンテキストでは文字はボックス化されます。 + +:::comment ## API Reference +::: + +## API リファレンス（API Reference） + +:::comment ### Character Classes +::: + +### 文字クラス（Character Classes） + {docstring Char.isAlpha} {docstring Char.isAlphanum} diff --git a/Manual/BasicTypes/Nat.lean b/Manual/BasicTypes/Nat.lean index ebc4e8c..4c24232 100644 --- a/Manual/BasicTypes/Nat.lean +++ b/Manual/BasicTypes/Nat.lean @@ -12,20 +12,43 @@ open Manual.FFIDocType open Verso.Genre Manual +/- #doc (Manual) "Natural Numbers" => +-/ +#doc (Manual) "自然数（Natural Numbers）" => +:::comment The natural numbers are nonnegative integers. Logically, they are the numbers 0, 1, 2, 3, …, generated from the constructors {lean}`Nat.zero` and {lean}`Nat.succ`. Lean imposes no upper bound on the representation of natural numbers other than physical constraints imposed by the available memory of the computer. +::: + +自然数は非負の整数です。論理的には 0・1・2・3・……であり、コンストラクタ {lean}`Nat.zero` と {lean}`Nat.succ` から生成されます。Lean はコンピュータの利用可能なメモリによって課される物理的制約以外に、自然数の表現に上限を課していません。 + +:::comment Because the natural numbers are fundamental to both mathematical reasoning and programming, they are specially supported by Lean's implementation. The logical model of the natural numbers is as an inductive datatype, and arithmetic operations are specified using this model. In Lean's kernel, the interpreter, and compiled code, closed natural numbers are represented as efficient arbitrary-precision integers. Sufficiently small numbers are immediate values that don't require indirection through a pointer. Arithmetic operations are implemented by primitives that take advantage of the efficient representations. +::: + +自然数は数学的推論とプログラミングの基本であるため、Lean の実装では特別なサポートを受けています。自然数の論理モデルは帰納的データ型であり、算術演算はこのモデルを用いて指定されます。Lean のカーネル・インタプリタ・コンパイルされたコードでは、閉じた自然数は効率的な任意精度の整数として表現されます。十分に小さい数値はポインタによるインダイレクトを必要としない即値です。算術演算は効率的な表現を利用するプリミティブによって実装されます。 + +:::comment # Logical Model +::: + +# 論理モデル（Logical Model） + {docstring Nat} +:::comment The Peano axioms are a consequence of this definition. The induction principle generated for {lean}`Nat` is the one demanded by the axiom of induction: +::: + +ペアノの公理はこの定義の帰結です。 {lean}`Nat` に対して生成される帰納原理は、帰納の公理が要求するものです。 + ```signature Nat.rec.{u} {motive : Nat → Sort u} (zero : motive zero) @@ -33,8 +56,13 @@ Nat.rec.{u} {motive : Nat → Sort u} (t : Nat) : motive t ``` +:::comment This induction principle also implements primitive recursion. The injectivity of {lean}`Nat.succ` and the disjointness of {lean}`Nat.succ` and `Nat.zero` are consequences of the induction principle, using a construction typically called “no confusion”: +::: + +この帰納原理は原始再帰も実装しています。 {lean}`Nat.succ` の単射性、 {lean}`Nat.succ` と `Nat.zero` の不連結性は一般的に「no confusion」と呼ばれる構造を用いた帰納原理の帰結です： + ```lean def NoConfusion : Nat → Nat → Prop | 0, 0 => True @@ -60,26 +88,56 @@ Look up and document ::: +:::comment ## Performance Notes +::: + +## パフォーマンスについての注記（Performance Notes） + +:::comment Using Lean's built-in arithmetic operators, rather than redefining them, is essential. The logical model of {lean}`Nat` is essentially a linked list, so addition would take time linear in the size of one argument. Still worse, multiplication takes quadradic time in this model. While defining arithmetic from scratch can be a useful learning exercise, these redefined operations will not be nearly as fast. +::: + +演算子について再定義せずに Lean の組み込み演算子を利用することが重要です。 {lean}`Nat` の論理モデルは基本的に連結リストであるため、足し算には引数のサイズに対して線形な時間がかかります。さらに悪いことに、このモデルでは掛け算に2乗の時間がかかります。0から算術演算を定義することは有用な学習の練習にはなりますが、これらの再定義された演算はほとんど速くなりません。 + +:::comment # Syntax +::: + +# 構文（Syntax） + +:::comment Natural number literals are overridden using the {lean}`OfNat` type class. +::: + +自然数リテラルは {lean}`OfNat` 型クラスを使って上書きされます。 + :::TODO Document this elsewhere, insert a cross-reference here ::: +:::comment # API Reference +::: + +# API リファレンス（API Reference） + +:::comment ## Arithmetic +::: + +## 算術（Arithmetic） + {docstring Nat.pred} {docstring Nat.add} @@ -98,8 +156,13 @@ Document this elsewhere, insert a cross-reference here {docstring Nat.log2} +:::comment ### Bitwise Operations +::: + +### ビット演算（Bitwise Operations） + {docstring Nat.shiftLeft} {docstring Nat.shiftRight} @@ -114,57 +177,102 @@ Document this elsewhere, insert a cross-reference here {docstring Nat.testBit} +:::comment ## Minimum and Maximum +::: + +## 最小・最大（Minimum and Maximum） + {docstring Nat.min} {docstring Nat.max} {docstring Nat.imax} +:::comment ## GCD and LCM +::: + +## 最大公約数と最小公倍数（GCD and LCM） + {docstring Nat.gcd} {docstring Nat.lcm} +:::comment ## Powers of Two +::: + +## 2の累乗（Powers of Two） + {docstring Nat.isPowerOfTwo} {docstring Nat.nextPowerOfTwo} +:::comment ## Comparisons +::: + +## 比較（Comparisons） + +:::comment ### Boolean Comparisons +::: + +### 真偽値の比較（Boolean Comparisons） + {docstring Nat.beq} {docstring Nat.ble} {docstring Nat.blt} +:::comment ### Decidable Equality +::: + +### 決定的な等価性（Decidable Equality） + {docstring Nat.decEq} {docstring Nat.decLe} {docstring Nat.decLt} +:::comment ### Predicates +::: + +### 述語（Predicates） + {docstring Nat.le} {docstring Nat.lt} {docstring Nat.lt_wfRel} +:::comment ## Iteration +::: + +## 反復（Iteration） + +:::comment Many iteration operators come in two versions: a structurally recursive version and a tail-recursive version. The structurally recursive version is typically easier to use in contexts where definitional equality is important, as it will compute when only some prefix of a natural number is known. +::: + +多くの反復演算子には、構造的再帰バージョンと末尾再帰バージョンの2種類があります。構造的再帰バージョンは自然数の接頭辞のみが分かっている場合に計算されるため、定義上の等価性が重要な文脈では一般的に使いやすいです。 + {docstring Nat.repeat} {docstring Nat.repeatTR} @@ -195,8 +303,13 @@ The structurally recursive version is typically easier to use in contexts where {docstring Nat.anyM} +:::comment ## Conversion +::: + +## 変換（Conversion） + {docstring Nat.toUInt8} {docstring Nat.toUInt16} @@ -231,23 +344,43 @@ The structurally recursive version is typically easier to use in contexts where {docstring Nat.superDigitChar} +:::comment ### Metaprogramming and Internals +::: + +### メタプログラミングと内部（Metaprogramming and Internals） + {docstring Nat.fromExpr?} {docstring Nat.toLevel} +:::comment ## Casts +::: + +## キャスト（Casts） + {docstring NatCast} {docstring Nat.cast} +:::comment ## Elimination +::: + +## 除去（Elimination） + +:::comment The recursion principle that is automatically generated for {lean}`Nat` results in proof goals that are phrased in terms of {lean}`Nat.zero` and {lean}`Nat.succ`. This is not particularly user-friendly, so an alternative logically-equivalent recursion principle is provided that results in goals that are phrased in terms of {lean}`0` and `n + 1`. +::: + +{lean}`Nat` に対して自動的に生成される再帰原理は、 {lean}`Nat.zero` と {lean}`Nat.succ` で表現される証明ゴールをもたらします。これは特にユーザフレンドリではないため、 {lean}`0` と `n + 1` で表現されたゴールとなる論理的に同値な別の再帰原理が提供されます。 + :::TODO Insert reference to section on how to do this ::: @@ -268,8 +401,13 @@ Insert reference to section on how to do this {docstring Nat.elimOffset} +:::comment ### Alternative Induction Principles +::: + +### 代替の帰納原理（Alternative Induction Principles） + {docstring Nat.strongInductionOn} {docstring Nat.caseStrongInductionOn} @@ -280,8 +418,13 @@ Insert reference to section on how to do this {docstring Nat.mod.inductionOn} +:::comment # Simplification +::: + +# 単純化（Simplification） + ## Normal Form :::TODO @@ -290,8 +433,13 @@ Document! ::: +:::comment ## Helpers +::: + +## 補助関数（Helpers） + {docstring Nat.isValue} {docstring Nat.reduceUnary} diff --git a/Manual/BasicTypes/String.lean b/Manual/BasicTypes/String.lean index d24731e..9ad82f6 100644 --- a/Manual/BasicTypes/String.lean +++ b/Manual/BasicTypes/String.lean @@ -20,64 +20,143 @@ set_option pp.rawOnError true example := Char +/- #doc (Manual) "Strings" => +-/ +#doc (Manual) "文字列（Strings）" => +:::comment Strings represent Unicode text. Strings are specially supported by Lean: * They have a _logical model_ that specifies their behavior in terms of lists of characters, which specifies the meaning of each operation on strings. * They have an optimized run-time representation in compiled code, as packed arrays of bytes that encode the string as UTF-8, and the Lean runtime specially optimizes string operations. * There is {ref "string-syntax"}[string literal syntax] for writing strings. +::: + +文字列は Unicode テキストを表現しています。文字列は Lean で特別にサポートされています： + * 文字のリストという観点から動作を指定する _論理モデル_ を持っており、文字列に対する各操作の意味を指定します。 + * コンパイルされたコードにおいて文字列を UTF-8 としてエンコードするバイトの packed array として最適化されたランタイム表現を持っており、Lean ランタイムは特別に文字列操作を最適化します。 + * 文字列を書くための {ref "string-syntax"}[文字列リテラルの構文] があります。 + +:::comment The fact that strings are internally represented as UTF-8-encoded byte arrays is visible in the API: * There is no operation to project a particular character out of the string, as this would be a performance trap. {ref "string-iterators"}[Use a {name}`String.Iterator`] in a loop instead of a {name}`Nat`. * Strings are indexed by {name}`String.Pos`, which internally records _byte counts_ rather than _character counts_, and thus takes constant time. Aside from `0`, these should not be constructed directly, but rather updated using {name}`String.next` and {name}`String.prev`. +::: + +文字列が内部的に UTF-8 エンコードされたバイト配列として表現されていることは API で確認できます： + * 文字列から特定の文字を射影する操作はありません（仮にあった場合パフォーマンスの罠になりえます）。 {name}`Nat` の代わりに {ref "string-iterators"}[{name}`String.Iterator`] をループ内で使ってください。 + * 文字列は {name}`String.Pos` によってインデックス付けされ、内部的には _文字数_ ではなく _バイト数_ を記録するため、一定の時間がかかります。`0` は別として、これらは直接構成されるのではなく、 {name}`String.next` と {name}`String.prev` をつかって更新されます。 + {include 0 Manual.BasicTypes.String.Logical} -# Run-Time Representation +# ランタイム表現（Run-Time Representation） %%% tag := "string-runtime" %%% +:::comment +# Run-Time Representation +::: + :::figure "Memory layout of strings" (name := "stringffi") ![Memory layout of strings](/static/figures/string.svg) ::: +:::comment Strings are represented as dynamic arrays of bytes, encoded in UTF-8. After the object header, a string contains: +::: + +文字列はバイトの動的配列として表現され、UTF-8 でエンコードされます。オブジェクトヘッダの後、文字列は以下を含みます： + +:::comment : byte count The number of bytes that currently contain valid string data +::: + +: バイト数 + + 現在有効な文字列データを含むバイト数 + +:::comment : capacity The number of bytes presently allocated for the string +::: + +: 容量 + + 現在文字列に割り当てられているバイト数 + +:::comment : length The length of the encoded string, which may be shorter than the byte count due to UTF-8 multibyte characters +::: + +: 長さ + + エンコードされた文字列の長さ。UTF-8 のマルチバイト文字のため、バイト数よりも短くなる可能性があります。 + +:::comment : data The actual character data in the string, null-terminated +::: + +: データ + + ヌル文字で終端された文字列内の実際の文字データ + +:::comment Many string functions in the Lean runtime check whether they have exclusive access to their argument by consulting the reference count in the object header. If they do, and the string's capacity is sufficient, then the existing string can be mutated rather than allocating fresh memory. Otherwise, a new string must be allocated. +::: + +Lean ランタイムの多くの文字列関数は、おぷじぇくとヘッダの参照カウントを参照することで引数に排他的アクセスがあるかどうかをチェックします。もしアクセスがあり、かつ文字列の容量が十分であれば、新しいメモリを確保するのではなく、既存の文字列を変更することができます。そうでない場合は新しい文字列を割り当てなければなりません。 + +:::comment ## Performance Notes +::: + +## パフォーマンスについての注記（Performance Notes） + +:::comment Despite the fact that they appear to be an ordinary constructor and projection, {name}`String.mk` and {name}`String.data` take *time linear in the length of the string*. This is because they must implement the conversions between lists of characters and packed arrays of bytes, which must necessarily visit each character. +::: + +一見普通のコンストラクタと射影に見えますが、 {name}`String.mk` と {name}`String.data` は *文字列の長さに比例した時間* がかかります。これは文字のリストとバイトの packed array の間の変換を実装しなければならないためで、各文字を必ず訪問しなければなりません。 + {include 0 Manual.BasicTypes.String.Literals} +# API リファレンス（API Reference） + +:::comment # API Reference +::: +:::comment ## Constructing +::: + +## 構成（Constructing） + {docstring String.singleton} {docstring String.append} @@ -86,8 +165,13 @@ This is because they must implement the conversions between lists of characters {docstring String.intercalate} +:::comment ## Conversions +::: + +## 変換（Conversions） + {docstring String.toList} {docstring String.isNat} @@ -104,16 +188,26 @@ This is because they must implement the conversions between lists of characters {docstring String.toFormat} +:::comment ## Properties +::: + +## プロパティ（Properties） + {docstring String.isEmpty} {docstring String.length} {docstring String.str} +:::comment ## Positions +::: + +## 位置（Positions） + {docstring String.Pos} {docstring String.Pos.isValid} @@ -134,8 +228,13 @@ This is because they must implement the conversions between lists of characters {docstring String.Pos.min} +:::comment ## Lookups and Modifications +::: + +## 検索と変更（Lookups and Modifications） + {docstring String.get} {docstring String.get?} @@ -195,8 +294,13 @@ This is because they must implement the conversions between lists of characters {docstring String.revFind} +:::comment ## Folds and Aggregation +::: + +## 畳み込みと集約（Folds and Aggregation） + {docstring String.map} {docstring String.foldl} @@ -207,8 +311,13 @@ This is because they must implement the conversions between lists of characters {docstring String.any} +:::comment ## Comparisons +::: + +## 比較（Comparisons） + {docstring String.le} {docstring String.firstDiffPos} @@ -225,8 +334,13 @@ This is because they must implement the conversions between lists of characters {docstring String.hash} +:::comment ## Manipulation +::: + +## 操作（Manipulation） + {docstring String.split} {docstring String.splitOn} @@ -243,15 +357,25 @@ This is because they must implement the conversions between lists of characters {docstring String.toLower} +:::comment ## Iterators +::: + +## イテレータ（Iterators） + %%% tag := "string-iterators" %%% +:::comment Fundamentally, a {name}`String.Iterator` is a pair of a string and a valid position in the string. Iterators provide functions for getting the current character ({name String.Iterator.curr}`curr`), replacing the current character ({name String.Iterator.setCurr}`setCurr`), checking whether the iterator can move to the left or the right ({name String.Iterator.hasPrev}`hasPrev` and {name String.Iterator.hasNext}`hasNext`, respectively), and moving the iterator ({name String.Iterator.prev}`prev` and {name String.Iterator.next}`next`, respectively). Clients are responsible for checking whether they've reached the beginning or end of the string; otherwise, the iterator ensures that its position always points at a character. +::: + +基本的に、 {name}`String.Iterator` は文字列と文字列内の有効な位置のペアです。イテレータは現在の文字を取得する関数（ {name String.Iterator.curr}`curr` ）・現在の文字を置き換える関数（ {name String.Iterator.setCurr}`setCurr` ）・イテレータが左または右に移動できるかどうかチェックする関数（それぞれ {name String.Iterator.hasPrev}`hasPrev` と {name String.Iterator.hasNext}`hasNext` ）・イテレータの移動（それぞれ {name String.Iterator.prev}`prev` と {name String.Iterator.next}`next` ）です。クライアントは文字列の先頭または末尾に到達したかどうかをチェックする責任があります；それ以外の場合、イテレータはその位置が常に文字を指すようにします。 + {docstring String.Iterator} {docstring String.iter} @@ -288,16 +412,26 @@ Clients are responsible for checking whether they've reached the beginning or en {docstring String.Iterator.pos} +:::comment ## Substrings +::: + +## 部分文字列（Substrings） + TODO Substring API xref {docstring String.toSubstring} {docstring String.toSubstring'} +:::comment ## Proof Automation +::: + +## 証明自動化（Proof Automation） + {docstring String.reduceGT} {docstring String.reduceGE} @@ -322,8 +456,13 @@ TODO Substring API xref {docstring String.reduceNe} +:::comment ## Metaprogramming +::: + +## メタプログラミング（Metaprogramming） + {docstring String.toName} {docstring String.toFileMap} @@ -332,8 +471,13 @@ TODO Substring API xref {docstring String.fromExpr?} +:::comment ## Encodings +::: + +## エンコード（Encodings） + {docstring String.utf16PosToCodepointPos} {docstring String.utf16PosToCodepointPosFrom} diff --git a/Manual/BasicTypes/String/FFI.lean b/Manual/BasicTypes/String/FFI.lean index 47fb18c..3ec0ecc 100644 --- a/Manual/BasicTypes/String/FFI.lean +++ b/Manual/BasicTypes/String/FFI.lean @@ -18,7 +18,7 @@ set_option pp.rawOnError true {docstring String.csize} -:::ffi "lean_string_object" kind := type +::::ffi "lean_string_object" kind := type ``` typedef struct { lean_object m_header; @@ -30,20 +30,35 @@ typedef struct { char m_data[0]; } lean_string_object; ``` +:::comment The representation of strings in C. See {ref "string-runtime"}[the description of run-time {name}`String`s] for more details. ::: -:::ffi "lean_is_string" +C での文字列の表現。詳細は {ref "string-runtime"}[{name}`String` のランタイムについての説明] を参照してください。 + +:::: + +::::ffi "lean_is_string" ```` bool lean_is_string(lean_object * o) ```` +:::comment Returns `true` if `o` is a string, or `false` otherwise. ::: -:::ffi "lean_to_string" +`o` が文字列であれば `true` を、そうでなければ `false` を返します。 + +:::: + +::::ffi "lean_to_string" ```` lean_string_object * lean_to_string(lean_object * o) ```` +:::comment Performs a runtime check that `o` is indeed a string. If `o` is not a string, an assertion fails. ::: + +`o` が本当に文字列であることのランタイムチェックの実行。`o` が文字列でない場合は失敗を主張します。 + +:::: diff --git a/Manual/BasicTypes/String/Literals.lean b/Manual/BasicTypes/String/Literals.lean index b6048f5..d2f4010 100644 --- a/Manual/BasicTypes/String/Literals.lean +++ b/Manual/BasicTypes/String/Literals.lean @@ -14,39 +14,88 @@ open Verso.Genre Manual set_option pp.rawOnError true +/- #doc (Manual) "Syntax" => +-/ +#doc (Manual) "構文（Syntax）" => %%% tag := "string-syntax" %%% +:::comment Lean has three kinds of string literals: ordinary string literals, interpolated string literals, and raw string literals. +::: + +Lean には3種類の文字列リテラルがあります：通常の文字列リテラル・補間文字列リテラル・生文字列リテラル + +:::comment # String Literals +::: + +# 文字列リテラル（String Literals） + +:::comment String literals begin and end with a double-quote character `"`. {index subterm:="string"}[literal] Between these characters, they may contain any other character, including newlines, which are included literally (with the caveat that all newlines in a Lean source file are interpreted as `'\n'`, regardless of file encoding and platform). Special characters that cannot otherwise be written in string literals may be escaped with a backslash, so `"\"Quotes\""` is a string literal that begins and ends with double quotes. The following forms of escape sequences are accepted: +::: + +文字列リテラルはダブルクォート文字 `"` で開始・終了します。 {index subterm:="string"}[literal] これらの文字の間には、改行文字を（文字通り）含む他の任意の文字を含めることができます（ただし、Lean ソースファイル内のすべての改行文字はファイルのエンコーディングやプラットフォームに関係なく `'\n'` として解釈されます）。文字列リテラルにかけない特殊文字はバックスラッシュでエスケープすることができるため、 `"\"Quotes\""` は二重引用符で開始・終了する文字列リテラルです。以下の形式のエスケープシーケンスが利用できます： + +:::comment : `\r`, `\n`, `\t`, `\\`, `\"`, `\'` These escape sequences have the usual meaning, mapping to `CR`, `LF`, tab, backslash, double quote, and single quote, respectively. +::: + +: `\r`・`\n`・`\t`・`\\`・`\"`・`\'` + + これらのエスケープシーケンスは通常の意味を持ち、それぞれ `CR`・`LF`・タブ・バックスラッシュ・二重引用符・引用符に対応します。 + +:::comment : `\xNN` When `NN` is a sequence of two hexadecimal digits, this escape denotes the character whose Unicode codepoint is indicated by the two-digit hexadecimal code. +::: + +: `\xNN` + + `NN` が2桁の16進数である時、このエスケープは2桁の16進数で示される Unicode コードポイントを持つ文字を表します。 + +:::comment : `\uNNNN` When `NN` is a sequence of two hexadecimal digits, this escape denotes the character whose Unicode codepoint is indicated by the four-digit hexadecimal code. +::: + +: `\uNNNN` + + `NN` が2桁の16進数である時、このエスケープは4桁の16進数コードで示される Unicode コードポイントを持つ文字を表します。 + +:::comment String literals may contain {deftech}[_gaps_]. A gap is indicated by an escaped newline, with no intervening characters between the escaping backslash and the newline. In this case, the string denoted by the literal is missing the newline and all leading whitespace from the next line. String gaps may not precede lines that contain only whitespace. +::: + +文字列リテラルは {deftech}[_ギャップ_] （gap）を含むことができます。ギャップはエスケープされた開業で示され、エスケープされたバックスラッシュと改行の間には文字が介在しません。この場合、リテラルで示される文字列には、改行と次の行の先頭の空白がすべて含まれません。文字列のギャップは空白のみを含む行の前にあってはなりません。 + +:::comment Here, `str1` and `str2` are the same string: +::: + + + ```lean def str1 := "String with \ a gap" @@ -55,53 +104,108 @@ def str2 := "String with a gap" example : str1 = str2 := rfl ``` +:::comment If the line following the gap is empty, the string is rejected: +::: + +ギャップに続く行が空の場合、その文字列は拒否されます： + ```syntaxError foo def str3 := "String with \ a gap" ``` +:::comment The parser error is: +::: + +パーサは以下のエラーを返します： + ```leanOutput foo :2:0: unexpected additional newline in string gap ``` +:::comment # Interpolated Strings +::: + +# 補間文字列（Interpolated Strings） + +:::comment Preceding a string literal with `s!` causes it to be processed as an {deftech}[_interpolated string_], in which regions of the string surrounded by `{` and `}` characters are parsed and interpreted as Lean expressions. Interpolated strings are interpreted by appending the string that precedes the interpolation, the expression (with an added call to {name ToString.toString}`toString` surrounding it), and the string that follows the interpolation. +::: + +文字列の前に `s!` を置くと、 {deftech}[_補間文字列_] （interpolated string）として処理されます。この文字列内の `{` と `}` で囲まれた領域がパースされ、Lean の式として解釈されます。補間文字列は、補間の前の文字列・式（それを囲む {name ToString.toString}`toString` の呼び出しが追加されたもの）・補間後の文字列が連結されたものとして解釈されます。 + +:::comment For example: +::: + +例えば： + ```lean example : s!"1 + 1 = {1 + 1}\n" = "1 + 1 = " ++ toString (1 + 1) ++ "\n" := rfl ``` +:::comment Preceding a literal with `m!` causes the interpolation to result in an instance of {name Lean.MessageData}`MessageData`, the compiler's internal data structure for messages to be shown to users. +::: + +リテラルの前に `m!` を置くと、 {name Lean.MessageData}`MessageData` のインスタンスとなります。これはコンパイラの内部からユーザ向けに使用されるメッセージのデータ構造です。 + +:::comment # Raw String Literals +::: + +# 生文字列リテラル + +:::comment In {deftech}[raw string literals], {index subterm:="raw string"}[literal] there are no escape sequences or gaps, and each character denotes itself exactly. Raw string literals are preceded by `r`, followed by zero or more hash characters (`#`) and a double quote `"`. The string literal is completed at a double quote that is followed by _the same number_ of hash characters. For example, they can be used to avoid the need to double-escape certain characters: +::: + +{deftech}[生文字列リテラル] {index subterm:="raw string"}[literal] （raw string literal）では、エスケープシーケンスやギャップはなく、各文字はそれ自身を正確に表します。生文字列リテラルは `r` で始まり、0個以上のハッシュ文字（`#`）と二重引用符 `"` が続きます。文字列リテラルは _同じ数_ のハッシュ文字が続く二重引用符で補完されます。例えば、特定の文字をダブルエスケープする必要を避けるために使用することができます： + ```lean (name := evalStr) example : r"\t" = "\\t" := rfl #eval r"Write backslash in a string using '\\\\'" ``` +:::comment The `#eval` yields: +::: + +この `#eval` は以下を出力します： + ```leanOutput evalStr "Write backslash in a string using '\\\\\\\\'" ``` +:::comment Including hash marks allows the strings to contain unescaped quotes: +::: + +ハッシュ記号を含めると、文字列にエスケープされていない引用符を含めることができます。 + ```lean example : r#"This is "literally" quoted"# = "This is \"literally\" quoted" := rfl ``` +:::comment Adding sufficiently many hash marks allows any raw literal to be written literally: +::: + +十分な数のハッシュ記号を追加することで、どんな生リテラルでも文字通りに書くことができます： + ```lean example : r##"This is r#"literally"# quoted"## = "This is r#\"literally\"# quoted" := rfl ``` diff --git a/Manual/BasicTypes/String/Logical.lean b/Manual/BasicTypes/String/Logical.lean index 1bce7f2..b953702 100644 --- a/Manual/BasicTypes/String/Logical.lean +++ b/Manual/BasicTypes/String/Logical.lean @@ -14,9 +14,17 @@ open Verso.Genre Manual set_option pp.rawOnError true +/- #doc (Manual) "Logical Model" => +-/ +#doc (Manual) "論理モデル（Logical Model）" => {docstring String} +:::comment The logical model of strings in Lean is a structure that contains a single field, which is a list of characters. This is convenient when specifying and proving properties of string-processing fuctions at a low level. + +::: + +Lean における文字列の論理モデルは、文字のリストである1つのフィールドを含む構造体です。これは低レベルで文字列処理関数のプロパティを指定したり証明したりするときに便利です。