perf: refactor rejectDuplicates in Parser.lean to avoid redundant sort and O(n²) insertion
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 45/100
- Issue type
- Refactor
- Clarity
- Mostly clear
- Activity status
- Stale
- Domain
- compilers, performance
Research direction
Start in Lck/Json/Parser.lean by reading SortedKVs.ofListWithPolicy, hasDuplicateKeysList, ofList, and ofListLastWins. Then inspect the existing structure in Syntax.lean and related proofs in Proofs.lean. Done means a fromSortedList helper enables one mergeSort pass for rejectDuplicates, firstWins, and lastWins while preserving the corresponding proofs and O(n log n) behavior.
Written by the indexing model from the issue text.
Description
Problem
SortedKVs.ofListWithPolicy .rejectDuplicates in Lck/Json/Parser.lean does two passes:
hasDuplicateKeysList: sorts the list (mergeSort, O(n log n)) then scans adjacent pairsSortedKVs.ofList: builds the sorted structure via repeatedinsert(O(n) each → O(n²) total)
Total cost is O(n log n) + O(n²) = O(n²) with a hidden constant from sorting twice.
Suggested Fix
Add a SortedKVs.fromSortedList helper that builds the sorted structure from a pre-sorted list in O(n), then combine the duplicate check and structure construction into a single pass over the mergeSort output. This would bring the rejectDuplicates path to O(n log n) overall.
The same refactor would help firstWins and lastWins paths in ofList/ofListLastWins.
Complexity
Moderate: requires a new Syntax.lean helper and corresponding proof in Proofs.lean.
- 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 ·