refactor: deduplicate Symbol.matches / charMatchesClass in Glushkov
Nobody has claimed this yet.
Assessment
- Difficulty
- 2/5
- Estimated time
- 1-3 hours
- Newbie friendliness
- 55/100
- Issue type
- Refactor
- Clarity
- Clearly specified
- Activity status
- Stale
- Domain
- compilers
Research direction
Start in Lck/Regex/Glushkov/Construction.lean at Symbol.matches and compare it with charMatchesClass in Syntax.lean. Then inspect the bridging have h_eq in Lck/Regex/Glushkov/CompositionCorrectness.lean; done means the duplication is removed and the proof is simplified without changing matching behavior.
Written by the indexing model from the issue text.
Description
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)
- Dominant language
- Lean
- Stars
- 2
- Forks
- 1
- PR merge metrics
- No merged PRs in 30d
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from lambdaclass/lambda_compiler_kit
-
Difficulty 1/5 Under an hour Newbie friendliness 72/100
-
Difficulty 1/5 Under an hour Newbie friendliness 68/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
-
enhancement
Difficulty 4/5 3-5 days Newbie friendliness 48/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 50/100
All issues in lambdaclass/lambda_compiler_kit
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
-
internal.h中，漏掉了1个定义。 Open
Difficulty 1/5 Under an hour Newbie friendliness 95/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
oxc-project/oxc#26944 ·