refactor: eliminate decreasing_by in Parser.lean in favour of structural recursion
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
- 42/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
Hướng nghiên cứu
Mở Lck/Regex/Parser.lean và kiểm tra mã phân tích cú pháp ở dòng 646 và 912, sau đó đọc hướng dẫn về tính kết thúc trong CLAUDE.md. Xác định xem các lời gọi đệ quy bị ảnh hưởng có thể sử dụng các danh sách token nhỏ hơn về mặt cấu trúc hay không; được xem là hoàn tất khi cả hai chỗ sử dụng decreasing_by đều được loại bỏ, hoặc một chú thích giải thích ghi lại lý do không thể tái cấu trúc.
Do mô hình lập chỉ mục viết ra từ nội dung của issue.
Mô tả
Problem
Lck/Regex/Parser.lean at lines 646 and 912 uses decreasing_by to convince the termination checker. Per CLAUDE.md, decreasing_by is a code smell for parsers — a well-structured LL(1) parser over a token list should terminate structurally.
Expected fix
Restructure the affected parsing functions so that recursive calls are made on a syntactically smaller token list, allowing the Lean termination checker to accept them without decreasing_by. If this turns out to be infeasible, document why with a comment.
References
- Observed by AI code review on PR #9
- See CLAUDE.md termination discipline
- 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