enhancementgood first issue
仓库指标
- 星标
- (109 个星标)
- PR 合并指标
- (PR 指标待抓取)
描述
Improve parser error messages with context
Description
Enhance the regex parser's error reporting to provide more helpful context and suggestions for common mistakes, making the library more beginner-friendly.
Current State
The parser has basic error types in regex/Regex/Syntax/Parser/Error.lean but error messages are quite generic:
- "unexpected character: )"
- "unexpected escaped character: q"
- "invalid range: z..a"
Proposed Implementation
Add contextual information and suggestions to error messages.
Implementation Steps
-
Enhanced Error Types:
- Add position information to errors
- Include surrounding context in error messages
- Add suggestion fields for common fixes
-
Improved ToString Implementation:
- Show position in input string where error occurred
- Provide helpful suggestions for common mistakes
- Format errors in a user-friendly way
-
Common Error Patterns:
- Unmatched parentheses: suggest missing
) - Invalid escapes: suggest valid alternatives
- Invalid ranges: explain correct range syntax
- Unmatched parentheses: suggest missing
Example Improvements
Before:
unexpected escaped character: q
After:
unexpected escaped character '\q' at position 5
regex: "hello\qworld"
^
suggestion: did you mean '\n' (newline) or remove the backslash?
Files to Modify
regex/Regex/Syntax/Parser/Error.lean- Add new error types and better ToStringregex/Regex/Syntax/Parser/Basic.lean- Include position info in errors
Testing
Add test cases for various error scenarios to ensure helpful messages are generated.
Skills Required
- Basic functional programming
- String formatting and manipulation
- No Lean theorem proving experience needed
Expected Outcome
Users get clear, actionable error messages when their regex syntax is invalid, improving the learning experience.