pandaman64/lean-regex

Improve parser error messages with context

开放

#94 创建于 2025年6月8日

 (0 条评论) (0 个反应) (0 位负责人)Lean (14 个派生)auto 404
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

  1. Enhanced Error Types:

    • Add position information to errors
    • Include surrounding context in error messages
    • Add suggestion fields for common fixes
  2. Improved ToString Implementation:

    • Show position in input string where error occurred
    • Provide helpful suggestions for common mistakes
    • Format errors in a user-friendly way
  3. Common Error Patterns:

    • Unmatched parentheses: suggest missing )
    • Invalid escapes: suggest valid alternatives
    • Invalid ranges: explain correct range syntax

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 ToString
  • regex/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.

贡献者指南