perf: refactor rejectDuplicates in Parser.lean to avoid redundant sort and O(n²) insertion
Chưa có ai nhận issue này.
Đánh giá
- Độ khó
- 4/5
- Thời gian dự kiến
- 3-5 ngày
- Mức phù hợp với người mới
- 45/100
- Loại issue
- Tái cấu trúc
- Độ rõ ràng
- Khá rõ ràng
- Mức độ hoạt động
- Đình trệ
- Lĩnh vực
- compilers, performance
Hướng nghiên cứu
Bắt đầu trong Lck/Json/Parser.lean bằng cách đọc SortedKVs.ofListWithPolicy, hasDuplicateKeysList, ofList và ofListLastWins. Sau đó kiểm tra cấu trúc hiện có trong Syntax.lean và các chứng minh liên quan trong Proofs.lean. Hoàn thành khi một helper fromSortedList cho phép thực hiện một lần mergeSort cho rejectDuplicates, firstWins và lastWins, đồng thời giữ nguyên các chứng minh tương ứng và hành vi O(n log n).
Do mô hình lập chỉ mục viết ra từ nội dung của issue.
Mô tả
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.
- Ngôn ngữ chính
- Lean
- Star
- 2
- Fork
- 1
- Chỉ số merge pull request
- Không có pull request nào được merge trong 30 ngày
Hướng dẫn đóng góp
Chưa lập chỉ mục được hướng dẫn đóng góp cho kho mã nguồn này
Bắt đầu từ đâu
- Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
- Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
- Fork repository và làm thay đổi trên một nhánh.
- Mở pull request có tham chiếu số hiệu của issue.
Issue khác của lambdaclass/lambda_compiler_kit
-
Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 72/100
-
Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 68/100
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 68/100
-
enhancement
Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 48/100
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 50/100
Tất cả issue của lambdaclass/lambda_compiler_kit
Issue tương tự
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 75/100
objectionary/eo#8923 ·
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 75/100
-
Coarray integration tests carry no LABELS, so run_tests.py silently skips them under every backend Đang mởcoarray
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 70/100
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 75/100
-
internal.h中，漏掉了1个定义。 Đang mở
Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 95/100