refactor: deduplicate Symbol.matches / charMatchesClass in Glushkov
还没有人认领这个 Issue。
评估
- 难度
- 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 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库，在一个分支上完成修改。
- 提交 Pull Request，并在描述里引用这个 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
objectionary/eo#8923 ·
-
难度 2/5 1-3 小时 新手友好度 75/100
-
Coarray integration tests carry no LABELS, so run_tests.py silently skips them under every backend 未关闭coarray
难度 2/5 1-3 小时 新手友好度 70/100
-
难度 2/5 1-3 小时 新手友好度 75/100
-
难度 1/5 1 小时以内 新手友好度 95/100