pandaman64/lean-regex

Correctly fail invalid range operators

オープン

#152 opened on 2025/12/30

 (0 件のコメント) (1 件のリアクション) (0 人の担当者)Lean (14 件のフォーク)auto 404
bughelp wanted

Repository metrics

Stars
 (109 個のスター)
PR merge metrics
 (PR metrics pending)

説明

We have extended the bracketed character class parsers with new capabilities like #150 while breaking error handling of range operators. Namely,

  • [z-a] should be an error (as the range is valid only if 'z' ≦ 'a'), but is treated as a union of z, -, and a.
  • Also, [\d-a] should be an error, but accepted as a union

We want to restore the original behavior that returns .error .invalidRange in such cases.

I'd expect that we need a rework of the bracketed class parsers to conform to a grammar like this:

escapedChar   ::= '\' c
singleChar    ::= c (except for '[', ']', '\', ...)
atom          ::= escapedChar | singleChar
rangeExpr     ::= atom ('-' atom)?
setOp         ::= '&&' | '||' | '--' | '~~'
setExpr       ::= bracketed (setOp bracketed)*
singleExpr    ::= rangeExpr | setExpr
bracketed     ::= '[' ('^')? singleExpr* ']'

The idea is to make a range expression a proper level in the hierarchy and insert .commit at appropriate levels.

コントリビューターガイド