refactor: deduplicate Symbol.matches / charMatchesClass in Glushkov
まだ誰も着手していません。
評価
- 難易度
- 2/5
- 見積もり時間
- 1〜3時間
- 初心者へのやさしさ
- 55/100
- issue の種類
- リファクタリング
- 明瞭さ
- 明確に書かれている
- 活発さ
- 停滞
- 領域
- compilers
調査の方向性
Lck/Regex/Glushkov/Construction.lean の Symbol.matches から始め、Syntax.lean の charMatchesClass と比較します。次に、Lck/Regex/Glushkov/CompositionCorrectness.lean の橋渡しをしている have h_eq を調べます。重複が除去され、マッチング動作を変更せずに証明が簡略化されれば完了です。
索引モデルが issue の本文から書いたものです。
説明
Problem
Symbol.matches (Construction.lean:138) reimplements the same character-class matching logic already present in charMatchesClass (Syntax.lean:74). This duplication has been noticed in a correctness proof: CompositionCorrectness.lean even contains an explicit bridging lemma:
have h_eq : Symbol.matches ... = charMatchesClass c ranges.ranges ...
Proposed fix
Rewrite Symbol.matches to delegate to charMatchesClass, eliminating the duplication:
def Symbol.matches (sym : Symbol) (c : Char) : Bool :=
match sym with
| Symbol.charClass ranges negated => charMatchesClass c ranges.ranges negated
The bridging have h_eq lemma in CompositionCorrectness becomes trivial (or can be removed via rfl/simp).
Impact
Low risk. Symbol.matches is called internally by the Glushkov matcher. The semantics are identical by construction — the existing bridge lemma proves this. No API change.
Scope
Lck/Regex/Glushkov/Construction.leanLck/Regex/Glushkov/CompositionCorrectness.lean(remove/simplify bridge lemma)
- 主要言語
- Lean
- スター
- 2
- フォーク
- 1
- PR マージ指標
- 30日以内にマージされた PR はありません
コントリビューションガイド
このリポジトリのコントリビューションガイドは索引されていません
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
lambdaclass/lambda_compiler_kit のほかの issue
-
難易度 1/5 1時間未満 初心者へのやさしさ 72/100
-
難易度 1/5 1時間未満 初心者へのやさしさ 68/100
-
難易度 2/5 1〜3時間 初心者へのやさしさ 68/100
-
enhancement
難易度 4/5 3〜5日 初心者へのやさしさ 48/100
-
難易度 2/5 1〜3時間 初心者へのやさしさ 50/100
lambdaclass/lambda_compiler_kit の issue をすべて見る
似ている issue
-
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
-
internal.h中，漏掉了1个定义。 オープン
難易度 1/5 1時間未満 初心者へのやさしさ 95/100
-
難易度 2/5 1〜3時間 初心者へのやさしさ 88/100
-
難易度 2/5 1〜3時間 初心者へのやさしさ 88/100
-
難易度 2/5 1〜3時間 初心者へのやさしさ 88/100
oxc-project/oxc#26944 ·