From 1fe1d6fef029b62a40676dfc22a328fd5430a61c Mon Sep 17 00:00:00 2001 From: Seasawher Date: Tue, 24 Sep 2024 15:36:46 +0900 Subject: [PATCH] =?UTF-8?q?precedence=20=E3=81=AF=E3=80=8C=EF=BC=88?= =?UTF-8?q?=E3=83=91=E3=83=BC=E3=82=B9=E3=81=AE=EF=BC=89=E5=84=AA=E5=85=88?= =?UTF-8?q?=E5=BA=A6=E3=80=8D=E3=81=A7=E3=81=AF=E3=81=AA=E3=81=8F=E3=81=A6?= =?UTF-8?q?=E3=80=8C=EF=BC=88=E3=83=91=E3=83=BC=E3=82=B9=E3=81=AE=EF=BC=89?= =?UTF-8?q?=E5=84=AA=E5=85=88=E9=A0=86=E4=BD=8D=E3=80=8D=E3=81=A8=E8=A8=B3?= =?UTF-8?q?=E3=81=99=20Fixes=20#873?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Declarative/Infix.lean | 8 +++---- Examples/Declarative/Notation.lean | 36 +++++++++++++++--------------- Examples/Declarative/Syntax.lean | 6 ++--- 3 files changed, 25 insertions(+), 25 deletions(-) diff --git a/Examples/Declarative/Infix.lean b/Examples/Declarative/Infix.lean index a6ea2de5..feeebab5 100644 --- a/Examples/Declarative/Infix.lean +++ b/Examples/Declarative/Infix.lean @@ -13,16 +13,16 @@ scoped infix:60 " ⋄ " => Nat.mul #guard 2 ⋄ 3 = 6 -/- `:` の後に付けている数字はパース優先度で、高いほど結合するタイミングが早くなります。等号 `=` のパース優先度は 50 であることを覚えておくと良いかもしれません。-/ +/- `:` の後に付けている数字はパース優先順位で、高いほど結合するタイミングが早くなります。等号 `=` のパース優先順位は 50 であることを覚えておくと良いかもしれません。-/ --- 等号より微妙にパース優先度が高い +-- 等号より微妙にパース優先順位が高い scoped infix:51 " strong " => Nat.add -- きちんと 1 + (2 strong 3) = 6 と解釈される。 --- これは、 等号のパース優先度が 51 未満であることを意味する +-- これは、 等号のパース優先順位が 51 未満であることを意味する #check 1 + 2 strong 3 = 6 --- パース優先度を 50 より小さくすると等号より低くなる +-- パース優先順位を 50 より低くすると等号より低くなる -- したがってエラーになる scoped infix:49 " weak " => Nat.add diff --git a/Examples/Declarative/Notation.lean b/Examples/Declarative/Notation.lean index 7c598564..13bf6ade 100644 --- a/Examples/Declarative/Notation.lean +++ b/Examples/Declarative/Notation.lean @@ -35,8 +35,8 @@ set_option pp.notation false end -/- ## パース優先度 -`notation` で記法を定義するときに、その記法の他の演算子などと比べたパース優先度(parsing precedence)を数値で指定することができます。パース優先度が高い演算子ほど、他の演算子より先に適用されます。言い換えれば、パース優先度を正しく設定することにより、括弧を省略しても意図通りに式が解釈されるようにすることができます。 +/- ## パース優先順位 +`notation` で記法を定義するときに、その記法の他の演算子などと比べたパース優先順位(parsing precedence)を数値で指定することができます。パース優先順位が高い演算子ほど、他の演算子より先に適用されます。言い換えれば、パース優先順位を正しく設定することにより、括弧を省略しても意図通りに式が解釈されるようにすることができます。 -/ /-- 結合が弱い方。中身は足し算 -/ @@ -46,7 +46,7 @@ notation:0 a:0 " weak " b:0 => Nat.add a b notation:70 a:70 " strong " b:70 => Nat.mul a b example : (3 weak 1 strong 2) = 5 := calc - -- weak と strong のパース優先度は strong の方が高いので、 + -- weak と strong のパース優先順位は strong の方が高いので、 -- まず 1 strong 2 が計算されて 2 になり、 _ = (3 weak 2) := rfl -- その後 3 weak 2 が計算されて 5 になる。 @@ -56,11 +56,11 @@ example : (2 strong 2 weak 3) = 7 := calc _ = (4 weak 3) := rfl _ = 7 := rfl -/- ### プレースホルダのパース優先度 -プレースホルダのパース優先度の数字は、「この位置に来る記号は、指定された数字以上のパース優先度を持たなければならない」ことを意味します。下記の例の場合、仮に右結合になるとすると `LXOR` 自身のパース優先度が `60` でしかなくて `61` 以上という制約を満たさないため、右結合になることがありえないことがわかります。 +/- ### プレースホルダのパース優先順位 +プレースホルダのパース優先順位の数字は、「この位置に来る記号は、指定された数字以上のパース優先順位を持たなければならない」ことを意味します。下記の例の場合、仮に右結合になるとすると `LXOR` 自身のパース優先順位が `60` でしかなくて `61` 以上という制約を満たさないため、右結合になることがありえないことがわかります。 -/ --- 右側のプレースホルダのパース優先度を１だけ大きくした +-- 右側のプレースホルダのパース優先順位を１だけ高くした notation:60 a:60 " LXOR " b:61 => !a && b -- 左結合だった場合の値 @@ -83,13 +83,13 @@ notation:60 a:61 " RXOR " b:60 => a && !b -- 右結合になることがわかる #guard true RXOR false RXOR true = true -/- ### パース優先度を省略した場合 -パース優先度を省略することもできるのですが、とても意外な挙動になるので推奨できません。なるべく全てのパース優先度を指定してください。-/ +/- ### パース優先順位を省略した場合 +パース優先順位を省略することもできるのですが、とても意外な挙動になるので推奨できません。なるべく全てのパース優先順位を指定してください。-/ -/-- パース優先度を全く指定しないで定義した記法。中身はべき乗 -/ +/-- パース優先順位を全く指定しないで定義した記法。中身はべき乗 -/ notation a " bad_pow " b => Nat.pow a b --- bad_pow のパース優先度は weak (優先度0)よりも低い？ +-- bad_pow のパース優先順位は weak (優先順位0)よりも低い？ example : (2 bad_pow 1 weak 3) = 16 := calc _ = (2 bad_pow 4) := rfl _ = 16 := rfl @@ -106,22 +106,22 @@ example : (2 weak 3 bad_pow 1 weak 2) = 29 := calc _ = (2 weak 27) := rfl _ = 29 := rfl -/- パース優先度を一部だけ指定しても効果がなく、強制的に右結合扱いになります。-/ +/- パース優先順位を一部だけ指定しても効果がなく、強制的に右結合扱いになります。-/ -/-- プレースホルダのパース優先度を省略した weak -/ +/-- プレースホルダのパース優先順位を省略した weak -/ notation:20 a " bad_weak" b => Nat.add a b -/-- プレースホルダのパース優先度を省略した strong -/ +/-- プレースホルダのパース優先順位を省略した strong -/ notation:70 a " bad_strong " b => Nat.mul a b --- bad_strong の方がパース優先度が高いと思いきや、 +-- bad_strong の方がパース優先順位が高いと思いきや、 -- 右結合になるので bad_weak の方が先に適用されてしまう example : (2 bad_strong 2 bad_weak 3) = 10 := calc _ = (2 bad_strong 5) := rfl _ = 10 := rfl /- ## 記法の重複問題 -`notation` を使って定義した記法のパース優先度が意図通りに反映されないことがあります。-/ +`notation` を使って定義した記法のパース優先順位が意図通りに反映されないことがあります。-/ section --# -- 排他的論理和の記号を定義 @@ -130,7 +130,7 @@ local notation:60 x:60 " ⊕ " y:61 => xor x y -- メタ変数を表示させないため set_option pp.mvars false --- 等号（パース優先度 50）より優先度が低いという問題でエラーになる +-- 等号（パース優先順位 50）より優先順位が低いという問題でエラーになる -- 上では60で定義しているのに、なぜ？ #check_failure true ⊕ true = false @@ -139,10 +139,10 @@ set_option pp.mvars false end --# -/- ここでのエラーの原因は、記法が被っていることです。`⊕` という記法は型の直和に対して既に使用されており、直和記法のパース優先度が等号より低いためにエラーが発生していました。-/ +/- ここでのエラーの原因は、記法が被っていることです。`⊕` という記法は型の直和に対して既に使用されており、直和記法のパース優先順位が等号より低いためにエラーが発生していました。-/ -- 集合の直和の記号と被っていた。 --- 集合の直和記号は等号よりパース優先度が低いからエラーになっていた +-- 集合の直和記号は等号よりパース優先順位が低いからエラーになっていた #check Nat ⊕ Fin 2 /- この問題の解決策は、まず第一に括弧を付けることですが、裏技として記法を上書きしてしまうこともできます。-/ diff --git a/Examples/Declarative/Syntax.lean b/Examples/Declarative/Syntax.lean index 563790fd..73557383 100644 --- a/Examples/Declarative/Syntax.lean +++ b/Examples/Declarative/Syntax.lean @@ -34,7 +34,7 @@ syntax "#greet" : command macro_rules | `(command| #greet) => `(#eval "Hello, Lean!") -/- ## パース優先度 +/- ## パース優先順位 `syntax` コマンドは Lean に新しい構文解析ルールを追加するので、既存の構文と衝突して意図通りに解釈されないことがあります。 -/ section @@ -57,10 +57,10 @@ Additional diagnostic information may be available using the `set_option diagnos #check_failure (1 + 1 = 2 as Nat) end -/- パース優先度(parsing precedence)を設定することで、どの構文から順に解釈されるかを指定することができ、問題を修正できることがあります。このあたりは [`notation`](./Notation.md) コマンドと同様です。 -/ +/- パース優先順位(parsing precedence)を設定することで、どの構文から順に解釈されるかを指定することができ、問題を修正できることがあります。このあたりは [`notation`](./Notation.md) コマンドと同様です。 -/ section --- 十分低いパース優先度を設定する +-- 十分低いパース優先順位を設定する local syntax:10 term:10 " = " term:10 " as " term:10 : term local macro_rules