Skip to content

Unicode RL1.5 support: Implement Case-Insensitive Matching Mode - #151

Merged
pandaman64 merged 17 commits into
pandaman64:mainfrom
yuuki14202028:feature/140-loose
Feb 22, 2026
Merged

Unicode RL1.5 support: Implement Case-Insensitive Matching Mode#151
pandaman64 merged 17 commits into
pandaman64:mainfrom
yuuki14202028:feature/140-loose

Conversation

@yuuki14202028

@yuuki14202028 yuuki14202028 commented Dec 28, 2025

Copy link
Copy Markdown
Contributor

Summary

This PR implements case-insensitive matching support using the (?i) inline flag modifier, addressing #140.

Changes

  • Added (?i) and (?-i) flag modifier parsing in Regex/Syntax/Parser/Basic.lean
  • Introduced Ast.flags node to represent inline flag modifiers in the AST
  • Refactored Ast.toRegexAux from index-based to state-based transformation using ToRegexState to track both group index and case-insensitivity flag
  • Created Regex/Unicode/CaseFold.lean implementing Unicode Simple Case Folding (status C+S from UCD CaseFolding.txt)
  • Added getCaseFoldEquivChars to generate character equivalence classes for case-insensitive matching
  • Included Unicode 17.0 Simple Case Folding data in regex/data/

Implementation Notes

  • Case-insensitive matching expands each character to an alternation of its case-equivalent characters (e.g., (?i)a becomes a|A)
  • Uses Simple Case Folding for single-character mappings only (Full Case Folding with multi-character expansions like ß→ss is not supported)
  • Flag scope follows standard regex semantics: (?i) enables and (?-i) disables case-insensitivity for subsequent patterns

Todo

  • Added parser tests for (?i) and (?-i) syntax in Parser/Test.lean
  • Support combining flags with non-capturing groups (e.g., (?i:abc))
  • Add edge case tests for multi-character case equivalence (e.g., Σ/σ/ς, K/k/K)
  • Add generate script Simple_Case_Folding.txt with .lean
  • Add caseInsensitive option to Regex.parse and Regex.parse! methods
  • Update correctness/ proofs to accommodate Ast.flags and ToRegexState changes
  • (Optional) Support case-insensitive matching for character class ranges (e.g., (?i)[a-z])

@pandaman64 pandaman64 left a comment

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ありがとうございます!

まだドラフトですがいくつかコメントしました。

Comment thread regex/Regex/Test.lean Outdated
Comment thread regex/data/Simple_Case_Folding.txt
Comment thread regex/Regex/Syntax/Parser/Basic.lean
Comment thread regex/Regex/Unicode/CaseFold.lean
@pandaman64

Copy link
Copy Markdown
Owner

レビュー遅れます。すいません

Comment thread regex/Regex/Unicode/CaseFold.lean Outdated
Comment thread regex/Regex/Syntax/Ast.lean Outdated
Comment thread correctness/RegexCorrectness/Unicode/CaseFoldEquiv.lean Outdated
Comment thread correctness/RegexCorrectness/Unicode/CaseFoldBinarySearch.lean Outdated
Comment thread correctness/RegexCorrectness/Unicode/CaseFoldBinarySearch.lean Outdated
Comment thread regex/Regex/Unicode/CaseFold.lean Outdated
Comment thread regex/Regex/Unicode/CaseFold.lean Outdated
@pandaman64
pandaman64 marked this pull request as ready for review February 22, 2026 08:16

@pandaman64 pandaman64 left a comment

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

遅くなりましたが、マージしようと思います。コントリビューションありがとうございました!

@pandaman64
pandaman64 merged commit b7d5287 into pandaman64:main Feb 22, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants