pandaman64/lean-regex

Unicode RL1.4 support: Update Word Boundaries to Use Unicode Properties (`\b`, `\B`)

Aperta

#139 aperta il 25 nov 2025

 (0 commenti) (0 reazioni) (0 assegnatari)Lean (14 fork)auto 404
enhancementgood first issuehelp wantedunicode

Metriche repository

Star
 (109 stelle)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

(This issue is AI-generated and may contain an error. Please comment on the issue to discuss what we'll implement)

Difficulty: Intermediate
Dependencies: ⚠️ Requires RL1.2 (Properties) to be completed first
UTS#18 Requirement: RL1.4 Simple Word Boundaries

Summary

Current Status

🟡 50/100 - ASCII Only

Currently:

  • ✅ Word boundary infrastructure exists (\b and \B work)
  • ✅ Correct boundary detection logic
  • ASCII-only word character definition (doesn't match Greek Α, Japanese あ, etc.)
  • ❌ Doesn't include Unicode decimal digits
  • ❌ Doesn't include ZWJ/ZWNJ characters
  • ❌ Doesn't handle combining marks

UTS#18 Requirement

RL1.4 Simple Word Boundaries: To meet this requirement, an implementation shall extend the word boundary mechanism so that:

  1. The class of <word_character> includes all the Alphabetic values from the Unicode character database, plus the decimals (General_Category=Decimal_Number), and the U+200C ZERO WIDTH NON-JOINER and U+200D ZERO WIDTH JOINER (Join_Control=True).
  2. Nonspacing marks are never divided from their base characters, and otherwise ignored in locating boundaries.

Goals

Update word boundary detection to use Unicode properties:

  • ✅ Greek words: \bΓεια\b matches "Γεια" (hello in Greek)
  • ✅ Japanese: \bこんにちは\b matches entire word
  • ✅ Decimal digits: \b123\b where 123 uses Arabic-Indic digits (١٢٣)
  • ✅ Combining marks: café (where é = e + U+0301) has boundaries at start/end only

Acceptance Criteria

  • Update Char.isWordChar to use Unicode properties
  • Word characters include: Alphabetic + Decimal_Number + Join_Control
  • Handle combining marks correctly (never split from base character)
  • Tests with Greek, Cyrillic, Arabic, CJK, emoji
  • Backward compatible (ASCII word boundaries still work)
  • Performance: Fast lookups (not linear search)

Technical Details

Current Implementation

Location: regex/Regex/Data/String.lean:74-93

def Char.isWordChar (ch : Char) : Bool :=
  ch.isAlphanum || ch = '_'  -- ASCII only!

def isAtWordBoundary (it : Iterator) : Bool :=
  isCurrWord it != isPrevWord it

Problems:

  1. isAlphanum is ASCII-only:

    • ❌ Doesn't match Greek: Α, Β, Γ, ...
    • ❌ Doesn't match Cyrillic: А, Б, В, ...
    • ❌ Doesn't match CJK: 中, 文, ...
    • ❌ Doesn't match Japanese: あ, い, う, ...
  2. Doesn't include Unicode decimal digits:

    • ❌ Arabic-Indic: ٠ ١ ٢ ... (U+0660-U+0669)
    • ❌ Devanagari: ० १ २ ... (U+0966-U+096F)
    • ❌ Many more...
  3. Doesn't include ZWJ/ZWNJ:

    • ❌ U+200C (ZERO WIDTH NON-JOINER)
    • ❌ U+200D (ZERO WIDTH JOINER)
    • Used in complex scripts and emoji

What Needs to Change

1. New Word Character Definition

Per UTS#18 RL1.4:

word_char := \p{Alphabetic} | \p{Nd} | \u{200C} | \u{200D}

Where:

  • \p{Alphabetic} - Unicode Alphabetic property (broader than Letter)
  • \p{Nd} - General_Category = Decimal_Number
  • \u{200C} - ZERO WIDTH NON-JOINER
  • \u{200D} - ZERO WIDTH JOINER

2. Combining Marks Handling

Rule: Nonspacing marks (Mn, Mc, Me) are never divided from base characters.

This means:

  • café where é = e + ́ has word boundaries only at: |café|
  • Not: |cafe|́| (wrong - splits combining mark)

Implementation approach (stretch goal):

  • When checking boundary, if current or previous char is combining mark, don't place boundary
  • Simpler: Start with code point-based implementation, defer combining marks to future improvement

3. Implementation

Update Char.isWordChar:

-- regex/Regex/Data/String.lean

-- Requires RL1.2 (Unicode properties) to be completed first!
def Char.isWordChar (ch : Char) : Bool :=
  -- Use Unicode properties from RL1.2
  UnicodeProperty.isAlphabetic ch
  || UnicodeProperty.isDecimalNumber ch
  || ch.toNat == 0x200C  -- ZERO WIDTH NON-JOINER
  || ch.toNat == 0x200D  -- ZERO WIDTH JOINER

Handle combining marks (stretch goal):

def Char.isCombiningMark (ch : Char) : Bool :=
  let gc := UnicodeProperty.generalCategory ch
  gc == .Mn || gc == .Mc || gc == .Me

def isAtWordBoundary (it : Iterator) : Bool :=
  let currWord := isCurrWord it
  let prevWord := isPrevWord it
  
  -- Basic check: word vs non-word
  if currWord != prevWord then
    -- Additional check: don't break if curr or prev is combining mark
    -- (This is the "stretch goal" part)
    !(isCurrCombiningMark it || isPrevCombiningMark it)
  else
    false

Simpler version (start here):

  • Just update isWordChar to use Unicode properties
  • Handle combining marks as future improvement
  • Document this limitation

4. Key Files to Modify

  1. regex/Regex/Data/String.lean

    • Update Char.isWordChar function
    • Optionally add combining mark handling
  2. Tests

    • Update existing word boundary tests
    • Add Unicode word boundary tests

Testing

Test Cases

Add to regex/tests/WordBoundaryTest.lean (or similar):

Basic Unicode Word Boundaries

-- Greek
#guard "\\bΓεια\\b" matches "Γεια"
#guard "\\bΓεια\\b" matches "Γεια" in "Γεια σου"
#guard "\\bΓεια" matches "Γεια" at start of "Γεια σου"

-- Cyrillic
#guard "\\bПривет\\b" matches "Привет"
#guard "\\bПривет" matches "Привет" in "Привет мир"

-- Arabic
#guard "\\bمرحبا\\b" matches "مرحبا"

-- CJK
#guard "\\b中文\\b" matches "中文"
#guard "\\b日本語\\b" matches "日本語"

-- Japanese Hiragana
#guard "\\bこんにちは\\b" matches "こんにちは"

// Hebrew
#guard "\\bשלום\\b" matches "שלום"

Decimal Digits

-- ASCII digits (should still work)
#guard "\\b123\\b" matches "123"

-- Arabic-Indic digits
#guard "\\b[\\u{660}-\\u{669}]+\\b" matches "١٢٣"

-- Devanagari digits
#guard "\\b[\\u{966}-\\u{96F}]+\\b" matches "१२३"

// Mixed
#guard "\\babc123\\b" matches "abc123"
#guard "\\bαβγ123\\b" matches "αβγ123"  // Greek + digits

Zero-Width Joiners

-- Emoji with ZWJ (treated as word characters)
#guard "\\b\\u{1F468}\\u{200D}\\u{1F469}\\u{200D}\\u{1F467}\\b" matches "👨‍👩‍👧"
// Family emoji: man + ZWJ + woman + ZWJ + girl

// Complex scripts using ZWNJ
#guard word boundaries respect ZWNJ in Persian/Arabic text

Combining Marks (Stretch Goal)

-- French
#guard "\\bcafé\\b" matches "café" where é = e + U+0301
#guard "\\b" doesn't match between 'e' and combining acute

-- Multiple combining marks
#guard "\\bq̈̄\\b" matches "q̈̄"  // q + diaeresis + macron

// Normalized vs decomposed should work the same
#guard "\\bcafé\\b" matches both:
  - "café" (precomposed: U+00E9)
  - "café" (decomposed: e + U+0301)

Mixed Scripts

-- Latin + Greek
#guard "\\bHello\\b" matches "Hello" in "Hello Γεια"
#guard "\\bΓεια\\b" matches "Γεια" in "Hello Γεια"

-- At boundaries
#guard "\\b" matches at: "|Hello| |Γεια|"

-- Word char followed by non-word char
#guard "\\btest\\b" matches "test" in "test!"
#guard "\\bΓεια\\b" matches "Γεια" in "Γεια!"

Backward Compatibility

-- ASCII still works
#guard "\\bword\\b" matches "word"
#guard "\\bhello\\b" matches "hello" in "hello world"
#guard "\\b[A-Za-z]+\\b" matches "Test"

// Underscore (keep as word char for compatibility?)
#guard "\\b_var\\b" matches "_var"
#guard "\\bvar_name\\b" matches "var_name"

-- Note: May need to keep underscore for backward compat,
-- even though it's not in Unicode word char definition

Edge Cases

-- Empty string
#guard "\\b" matches at position 0 in ""

-- Start/end of string
#guard "^\\b" matches at start
#guard "\\b$" matches at end

// Adjacent word characters of different scripts
#guard "\\b" matches between: "Hello|Γεια"  // Latin-Greek boundary
// This is actually word boundary (space between)

-- Digits at boundaries
#guard "\\b123abc\\b" matches "123abc"
#guard "\\babc123\\b" matches "abc123"

-- Punctuation
#guard "\\bword\\b" matches "word" in "word."
#guard "\\bword\\b" matches "word" in "(word)"

-- Multiple boundaries in one string
#guard "\\b" matches 4 times in "hello world": |hello| |world|

Implementation Strategy

Phase 1: Basic Implementation (Days 1-3)

Goal: Update word char definition without combining marks.

  1. Verify RL1.2 dependency:

    • Check that Unicode properties are available
    • Test property access: UnicodeProperty.isAlphabetic
  2. Update Char.isWordChar:

    def Char.isWordChar (ch : Char) : Bool :=
      UnicodeProperty.isAlphabetic ch
      || UnicodeProperty.isDecimalNumber ch
      || ch.toNat == 0x200C
      || ch.toNat == 0x200D
      || ch == '_'  // Keep for backward compat? Discuss.
    
  3. Test basic cases:

    • ASCII (ensure no regression)
    • Greek, Cyrillic
    • CJK
    • Arabic

Phase 2: Combining Marks (Days 4-5, Stretch Goal)

Goal: Handle combining marks correctly.

  1. Add combining mark detection:

    def Char.isCombiningMark (ch : Char) : Bool := ...
    
  2. Update boundary detection:

    • Don't place boundary if adjacent to combining mark
  3. Test:

    • French, Vietnamese (many combining marks)
    • Normalized vs decomposed forms

Phase 3: Testing & Polish (Days 6-7)

  1. Comprehensive test suite
  2. Performance testing
  3. Documentation
  4. Backward compatibility check

Implementation Notes

Dependency on RL1.2

This issue cannot be implemented until RL1.2 is complete!

Required from RL1.2:

  • UnicodeProperty.isAlphabetic : Char → Bool
  • UnicodeProperty.isDecimalNumber : Char → Bool (or generalCategory ch == .Nd)
  • UnicodeProperty.generalCategory : Char → GeneralCategoryValue

Make sure these are available before starting.

Underscore Handling

Question: Should _ remain a word character?

Options:

  1. Keep it (recommended for backward compatibility)

    • Most programmers expect _ in identifiers
    • Common in variable names
  2. Remove it (strict UTS#18 compliance)

    • UTS#18 doesn't include _ in word characters
    • More consistent with Unicode definition

Recommendation: Keep it, document the extension.

Combining Marks Complexity

Handling combining marks correctly is complex:

  • Need grapheme cluster awareness
  • Multiple combining marks on one base
  • Ordering issues
  • Interaction with normalization

Recommendation: Start with simple code point-based implementation. Mark combining marks handling as "stretch goal" or "future improvement."

Performance Considerations

Property lookups must be fast:

  • ✅ Use 2-stage tables or hash maps
  • ✅ Cache common lookups
  • ❌ Don't iterate all code points

The boundary check happens frequently during matching, so it must be optimized.


Resources

  • UTS#18 Specification: UTS #18_ Unicode Regular Expressions.html (lines 2107-2145)
  • Compliance Analysis: uts18_compliance_check.md (lines 538-670)
  • UAX#29 (Text Segmentation): https://www.unicode.org/reports/tr29/
    • Defines word boundaries more precisely
    • RL1.4 is "simple", RL2.3 would use full UAX#29

Notes for Contributors

Getting Started

  1. Check RL1.2 first: Make sure Unicode properties are implemented
  2. Start simple: Just update word char definition
  3. Test incrementally: Add one script at a time
  4. Defer combining marks: Can be added later

Common Pitfalls

  • ❌ Don't break ASCII word boundaries (regression!)
  • ❌ Don't forget ZWJ/ZWNJ (important for emoji and complex scripts)
  • ❌ Don't do linear search through all code points
  • ✅ Do test with actual Unicode text (not just ASCII)
  • ✅ Do consider performance (boundary checks are frequent)
  • ✅ Do document any extensions (like keeping underscore)

Testing Strategy

  1. ASCII regression: Ensure all existing tests pass
  2. Unicode scripts: Test Greek, Cyrillic, Arabic, CJK, etc.
  3. Edge cases: Empty strings, start/end of string, mixed scripts
  4. Performance: Benchmark boundary detection speed
  5. Compatibility: Compare behavior with other regex engines

Questions?

  • Q: Should underscore remain a word character? A: Discuss with maintainers, but recommend keeping for compatibility.

  • Q: How to handle combining marks? A: Start without them (document limitation), add as future improvement.

  • Q: What about emoji modifiers? A: ZWJ/ZWNJ are included, modifiers work through that.


Related Issues

  • Requires: RL1.2 (Properties) - must be completed first!
  • Improves: Overall Unicode support in regex engine
  • Future: RL2.3 would add full UAX#29 word boundary support

Guida contributor