Unicode RL1.3 support: Add Set Operations in Character Classes (&&, --, ||, ~~) #138

[yuuki14202028]

This PR implements character class set operations (--, &&, ||, ~~) and nested character classes, addressing #138.
dependency: #149

Changes

• Refactored Classes type in Regex/Data/Classes.lean from a struct to an inductive type (ADT) supporting atom, complement, union, intersection, difference, and symDiff.
• Updated Regex.Syntax.Parser to parse nested character classes (e.g., [[a-z]--[aeiou]]) with left-to-right evaluation.
• Added set operator parsing for -- (difference), && (intersection), || (union), and ~~ (symmetric difference).
• Added test cases in regex/Regex/Syntax/Parser/Test.lean for set operations.

ToDo

• [[a-z]--[aeiou]]
• [a-z--[aeiou]]
• Optimized tree structure for set operations with matching functionality

[pandaman64]

PRありがとうございます！時間があるときにレビューします！

（今後はPRを送る前にIssueに一言コメントがあると助かります。被りを避けたいので）

[yuuki14202028]

了解です！

[yuuki14202028]

CorpusTestが落ちるのは副次的な問題で、下記の全てはRL1.2に関するものですが、[]の入れ子に対応したので結果が変わったのが原因です。
CorpusTestをcommitsに加えても良いですか？

diff --git a/regex/tests/CorpusTest.csv b/regex/tests/CorpusTest.csv
index fc13574..36776be 100644
--- a/regex/tests/CorpusTest.csv
+++ b/regex/tests/CorpusTest.csv
@@ -60,12 +60,12 @@ crazy/start-end-empty-rep,ok,
 crazy/start-end-empty-rep-rev,ok,
 crazy/neg-class-letter,ok,
 crazy/neg-class-letter-comma,ok,
-crazy/neg-class-letter-space,error,"expected '[^a[:space:]]' to compile, but it did not: expected EOF"
+crazy/neg-class-letter-space,error,"expected #[{ id := 0, spans := #[some { start := 2, end := 3 }] }], got #[#[(some (1, 2))], #[(some (2, 3))]]"
 crazy/neg-class-comma,ok,
-crazy/neg-class-space,error,"expected '[^[:space:]]' to compile, but it did not: expected EOF"
-crazy/neg-class-space-comma,error,"expected '[^,[:space:]]' to compile, but it did not: expected EOF"
-crazy/neg-class-comma-space,error,"expected '[^[:space:],]' to compile, but it did not: expected EOF"
-crazy/neg-class-ascii,error,"expected '[^[:alpha:]Z]' to compile, but it did not: expected EOF"
+crazy/neg-class-space,error,"expected #[{ id := 0, spans := #[some { start := 1, end := 2 }] }], but got #[#[(some (0, 1))]]"
+crazy/neg-class-space-comma,error,"expected #[{ id := 0, spans := #[some { start := 2, end := 3 }] }], but got #[#[(some (1, 2))]]"
+crazy/neg-class-comma-space,error,"expected #[{ id := 0, spans := #[some { start := 2, end := 3 }] }], but got #[#[(some (0, 1))]]"
+crazy/neg-class-ascii,error,"expected #[{ id := 0, spans := #[some { start := 1, end := 2 }] }], got #[#[(some (0, 1))], #[(some (1, 2))]]"
 crazy/lazy-many-many,ok,
 crazy/lazy-many-optional,ok,
 crazy/lazy-one-many-many,ok,
@@ -398,7 +398,7 @@ regression/unsorted-binary-search-200,error,"expected '(?i-u)[A_]+' to compile,
 regression/unicode-case-lower-nocase-flag,error,"expected '(?i)\p{Ll}+' to compile, but it did not: unexpected character: ?"
 regression/negated-char-class-100,error,"expected '(?i)[^x]' to compile, but it did not: unexpected character: ?"
 regression/negated-char-class-200,error,"expected '(?i)[^x]' to compile, but it did not: unexpected character: ?"
-regression/ascii-word-underscore,error,"expected '[[:word:]]' to compile, but it did not: expected EOF"
+regression/ascii-word-underscore,error,"expected #[{ id := 0, spans := #[some { start := 0, end := 1 }] }], got #[]"
 regression/captures-repeat,error,"expected '([a-f]){2}(?P<foo>[x-z])' to compile, but it did not: unexpected character: ?"
 regression/alt-in-alt-100,error,"expected #[{ id := 0, spans := #[some { start := 0, end := 1 }] }, { id := 0, spans := #[some { start := 2, end := 2 }] }], got #[#[(some (0, 1))], #[(some (2, 2))], #[(some (2, 2))]]"
 regression/alt-in-alt-200,ok,
@@ -441,8 +441,8 @@ regression/stops,unsupported,
 regression/stops-ascii,unsupported,
 regression/adjacent-line-boundary-100,error,"expected '(?m)^(?:[^ ]+?)$' to compile, but it did not: unexpected character: ?"
 regression/adjacent-line-boundary-200,error,"expected '(?m)^(?:[^ ]+?)$' to compile, but it did not: unexpected character: ?"
-regression/anchored-prefix-100,error,"expected '^a[[:^space:]]' to compile, but it did not: expected EOF"
-regression/anchored-prefix-200,error,"expected '^a[[:^space:]]' to compile, but it did not: expected EOF"
+regression/anchored-prefix-100,ok,
+regression/anchored-prefix-200,ok,
 regression/anchored-prefix-300,ok,
 regression/aho-corasick-100,ok,
 regression/interior-anchor-capture,ok,
@@ -473,7 +473,7 @@ regression/reverse-inner-plus-shorter-than-expected,ok,
 regression/reverse-inner-short,ok,
 regression/prefilter-with-aho-corasick-standard-semantics,unsupported,
 regression/non-prefix-literal-quit-state,ok,
-regression/hir-optimization-out-of-order-class,error,"expected '^[[:alnum:]./-]+$' to compile, but it did not: expected EOF"
+regression/hir-optimization-out-of-order-class,error,"expected #[{ id := 0, spans := #[some { start := 0, end := 3 }] }], got #[]"
 regression/improper-reverse-suffix-optimization,ok,
 set/basic10,unsupported,
 set/basic10-leftmost-first,unsupported,

[pandaman64]

報告ありがとうございます。CorpusTestの変更をコミットするのは問題ないのですが、[:alnum:]等のPOSIX文字クラスは現状パースエラーのままにしておきたいです（誤って使う可能性があるので）
[:のパース時に.error .unsupportedCharacterClassを返すように変更をお願いしてもいいですか？

CorpusTestの結果はcd regex/ && lake exe CorpusTest && lake exe CorpusTest --backtrackerで上書きできると思います（2つエンジンがあるのでそれぞれ上書きが必要です。）
ありがとうございます！

[yuuki14202028]

[:のパース時に.error .unsupportedCharacterClassを返すように変更をお願いしてもいいですか？

変更しました！
副作用として[:abc]みたいなものもエラーになってしまいますが、[abc:]のようにすれば回避できることと、RL1.2を実装すれば自然と解消されることを考慮してそのままにしています。

[pandaman64]

よくできています！細々とした点にコメントしました。

コントリビューションありがとうございます！

[pandaman64]

LGTMです！この状態で一回マージしようと思うのですが、どうでしょうか

[yuuki14202028]

ありがとうございます！大丈夫ですよ！

[pandaman64]

ありがとうございます！