Unicode RL1.2 support: Implement Unicode Properties (`\p{...}` and `\P{...}`)

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

Difficulty: Advanced - Most Critical Requirement
UTS#18 Requirement: RL1.2 Properties

Summary

Current Status

❌ 0/100 - Not Implemented

This is the most critical requirement for UTS#18 Level 1 conformance.

Currently, the regex engine only supports ASCII-based Perl classes:

• \d - ASCII digits (0-9)
• \s - ASCII whitespace
• \w - ASCII word characters (alphanumeric + underscore)

There is no support for Unicode properties like \p{Letter}, \p{Script=Greek}, etc.

UTS#18 Requirement

RL1.2 Properties: To meet this requirement, an implementation shall provide at least a minimal list of properties, consisting of the following:

• General_Category and Core Properties (Any, ASCII, Assigned)
• Script and Script_Extensions
• Alphabetic
• Uppercase
• Lowercase
• White_Space
• Noncharacter_Code_Point
• Default_Ignorable_Code_Point

Must support syntax: \p{Property}, \p{Property=Value}, \P{Property} (negated).

Goals

Implement Unicode property support to enable:

• ✅ \p{Letter} or \p{L} - All Unicode letters (not just ASCII)
• ✅ \p{Script=Greek} or \p{sc=Grek} - Greek script characters
• ✅ \p{Alphabetic} - Alphabetic characters (broader than Letter)
• ✅ \P{ASCII} - Negated property (all non-ASCII characters)
• ✅ Integration with other regex features (character classes, quantifiers, etc.)

Acceptance Criteria

• Investigation phase complete: Document UnicodeBasic library capabilities
• Data structures: Add UnicodeProperty type and update Class type
• Parser: Accept \p{...} and \P{...} syntax
• Property matching: All required properties implemented and working
• Property names: Support both long and short aliases (e.g., L and Letter)
• Property values: Support syntax like \p{Script=Greek} and \p{gc=Lu}
• Case-insensitive: Property names match case-insensitively
• Tests: Comprehensive tests for all properties and edge cases
• Documentation: Usage guide and examples

---

Technical Details

Current Implementation

Status: No Unicode property support exists.

Evidence from code:

1. Parser (regex/Regex/Syntax/Parser/Basic.lean:41-78):

   • Only Perl classes: \d, \s, \w (and negations)
   • No \p{...} or \P{...} support

2. Classes (regex/Regex/Data/Classes.lean:13):

   -- NOTE: we may want to interpret these as Unicode character properties in the future
   

3. ASCII-only definitions (regex/Regex/Data/Classes.lean:54-62):

   def PerlClassKind.mem (c : Char) (kind : PerlClassKind) : Bool :=
     match kind with
     | PerlClassKind.digit => c.isDigit       -- ASCII 0-9 only
     | PerlClassKind.space => c == ' ' || c == '\t' || c == '\n' || ...
     | PerlClassKind.word => c.isAlphanum || c == '_'  -- ASCII only
   

What Needs to Change

This is a major feature requiring changes across multiple components. We'll break it into phases.

Phase 1: Investigation

Goal: Determine if UnicodeBasic library meets our needs.

Tasks:

1. Create a document with:

   • What properties are available in UnicodeBasic
   • Which Unicode version it supports
   • API examples and usage patterns
   • Property value aliases support
   • Performance characteristics

2. Gap analysis:

   • Which RL1.2 properties are missing?
   • Can we contribute missing properties to UnicodeBasic?
   • Fallback strategy if UnicodeBasic isn't suitable?

Deliverable: Decision document on whether to use UnicodeBasic or alternative approach.

Phase 2: Data Structures

Goal: Extend the type system to represent Unicode properties.

Key files: regex/Regex/Data/Classes.lean

Add new types:

-- Enumerated property values
inductive GeneralCategoryValue where
  | Lu | Ll | Lt | Lm | Lo  -- Letter subcategories
  | Mn | Mc | Me              -- Mark
  | Nd | Nl | No              -- Number
  | Pc | Pd | Ps | Pe | Pi | Pf | Po  -- Punctuation
  | Sm | Sc | Sk | So         -- Symbol
  | Zs | Zl | Zp              -- Separator
  | Cc | Cf | Cs | Co | Cn    -- Other

inductive ScriptValue where
  | Common | Latin | Greek | Cyrillic | Arabic
  | Hebrew | Devanagari | Bengali | ... -- Many more

-- Unicode property representation
inductive UnicodeProperty where
  | generalCategory : GeneralCategoryValue → UnicodeProperty
  | script : ScriptValue → UnicodeProperty
  | scriptExtensions : ScriptValue → UnicodeProperty
  | alphabetic : UnicodeProperty
  | uppercase : UnicodeProperty
  | lowercase : UnicodeProperty
  | whiteSpace : UnicodeProperty
  | noncharacter : UnicodeProperty
  | defaultIgnorable : UnicodeProperty
  | any : UnicodeProperty
  | ascii : UnicodeProperty
  | assigned : UnicodeProperty

-- Update Class type
inductive Class where
  | single : Char → Class
  | range : (s : Char) → (e : Char) → Class
  | perl : PerlClass → Class
  | unicodeProperty : Bool → UnicodeProperty → Class  -- negated flag + property

Property matching interface:

-- regex/Regex/Data/UnicodeProperty.lean (new file)
namespace Regex.Data

def UnicodeProperty.matches (prop : UnicodeProperty) (c : Char) : Bool :=
  match prop with
  | .alphabetic => UnicodeBasic.isAlphabetic c
  | .generalCategory gc => matchesGeneralCategory c gc
  | .script s => UnicodeBasic.script c == s
  | .scriptExtensions s => s ∈ UnicodeBasic.scriptExtensions c
  | .whiteSpace => UnicodeBasic.isWhiteSpace c
  | .uppercase => UnicodeBasic.isUppercase c
  | .lowercase => UnicodeBasic.isLowercase c
  | .noncharacter => isNoncharacter c
  | .defaultIgnorable => isDefaultIgnorable c
  | .any => true
  | .ascii => c.toNat ≤ 0x7F
  | .assigned => c.toNat ≤ 0x10FFFF && ¬isUnassigned c

def Class.mem (c : Char) (cls : Class) : Bool :=
  match cls with
  | .single ch => c = ch
  | .range s e => s ≤ c && c ≤ e
  | .perl pc => PerlClass.mem c pc
  | .unicodeProperty negated prop =>
      let matches := prop.matches c
      if negated then !matches else matches

Phase 3: Parser

Goal: Parse \p{...} and \P{...} syntax.

Key files: regex/Regex/Syntax/Parser/Basic.lean

Add property parser:

-- Parse \p{PropertySpec} or \P{PropertySpec}
def unicodeProperty : Parser.LT Error Class := do
  let negated ← (charOrError '\\' *> ((charOrError 'p').map (fun _ => false)
                                   <|> (charOrError 'P').map (fun _ => true)))
  charOrError '{'
  let prop ← propertySpec
  charOrError '}'
  return .unicodeProperty negated prop

-- Parse property specification: Name or Name=Value
def propertySpec : Parser.LT Error UnicodeProperty := do
  let name ← propertyName
  let value ← optional (charOrError '=' *> propertyValue)
  return parseProperty name value

-- Property name (case-insensitive, spaces/hyphens/underscores ignored)
def propertyName : Parser.LT Error String := do
  -- Parse identifier
  -- Normalize: lowercase, remove spaces/hyphens/underscores
  -- Return normalized name

-- Property value (for Script, General_Category)
def propertyValue : Parser.LT Error String := do
  -- Similar normalization as propertyName

Property name matching (lenient per UTS#18):

All of these should be equivalent:

• \p{Lu} = \p{lu} = \p{Uppercase Letter} = \p{uppercase letter} = \p{Uppercase_Letter} = \p{uppercaseletter}

Normalization rules:

• Convert to lowercase
• Remove spaces, hyphens, underscores
• Match against both short and long aliases

Phase 4: Property Implementation (Weeks 4-5)

Goal: Implement all required properties.

Required Properties:

1. General_Category (30+ values):

   • Use UnicodeBasic or generate table from UnicodeData.txt
   • Support both category (L) and subcategory (Lu, Ll, etc.)

2. Core Properties:

   • Any - all code points (trivial: always true)
   • ASCII - U+0000 to U+007F
   • Assigned - all assigned characters (not Cn)

3. Script (150+ values):

   • Use UnicodeBasic or Scripts.txt
   • Support aliases (e.g., Greek = Grek)

4. Script_Extensions:

   • Like Script but with multiple values per character
   • U+30FC (ー) has Script=Common but ScriptExtensions={Hira, Kana}

5. Binary Properties:

   • Alphabetic - broader than General_Category=Letter
   • Uppercase - has uppercase
   • Lowercase - has lowercase
   • White_Space - Unicode whitespace
   • Noncharacter_Code_Point - 66 noncharacters
   • Default_Ignorable_Code_Point - format controls, etc.

Data source options:

1. Use UnicodeBasic library (preferred if complete)
2. Generate tables from Unicode data files at build time
3. Embed pre-generated tables

Phase 5: Testing (Week 6)

Goal: Comprehensive test coverage.

See "Testing" section below for details.

Key Files to Modify

1. regex/Regex/Data/Classes.lean

   • Add UnicodeProperty types
   • Update Class type
   • Update Class.mem function

2. regex/Regex/Data/UnicodeProperty.lean (new file)

   • Property matching logic
   • Property value enums
   • Helper functions

3. regex/Regex/Syntax/Parser/Basic.lean

   • Add unicodeProperty parser
   • Add propertySpec parser
   • Property name normalization

4. regex/Regex/Syntax/Parser/Error.lean

   • Add error variants: unknownProperty, invalidPropertyValue

5. regex/lakefile.toml

   • Add UnicodeBasic dependency (if used)

6. regex/tests/CorpusTest.lean

   • Enable more Unicode tests from testdata

---

Testing

Unit Tests

Add to regex/Regex/Syntax/Parser/Test.lean:

Parser Tests

-- Basic property syntax
#guard parseAst "\\p{L}" = .ok (.classes (Classes.mk false #[.unicodeProperty false .letter]))
#guard parseAst "\\p{Letter}" = .ok (...)
#guard parseAst "\\P{Letter}" = .ok (.classes (Classes.mk false #[.unicodeProperty true .letter]))

-- Property with value
#guard parseAst "\\p{Script=Greek}" = .ok (...)
#guard parseAst "\\p{sc=Grek}" = .ok (...)
#guard parseAst "\\p{General_Category=Lu}" = .ok (...)
#guard parseAst "\\p{gc=Lu}" = .ok (...)

-- Case insensitivity
#guard parseAst "\\p{uppercase letter}" = .ok (...)
#guard parseAst "\\p{UPPERCASE_LETTER}" = .ok (...)

-- In character classes
#guard parseAst "[\\p{L}\\p{N}]" = .ok (...)
#guard parseAst "[a-z\\p{Greek}]" = .ok (...)

-- Errors
#guard parseAst "\\p{InvalidProperty}" = .error (.unknownProperty "invalidproperty")
#guard parseAst "\\p{Script=FakeScript}" = .error (.invalidPropertyValue ...)
#guard parseAst "\\p{" = .error (.unexpectedEndOfInput)

Matching Tests

Create regex/tests/UnicodePropertyTest.lean:

-- General_Category
#guard "\\p{Lu}" matches "A"
#guard "\\p{Lu}" matches "Σ"  -- Greek uppercase sigma
#guard "\\p{Lu}" matches "Ж"  -- Cyrillic uppercase zhe
#guard "\\p{Lu}" doesn't match "a"
#guard "\\p{Lu}" doesn't match "5"

#guard "\\p{Ll}" matches "a"
#guard "\\p{Ll}" matches "α"  -- Greek lowercase alpha

#guard "\\p{Nd}" matches "5"
#guard "\\p{Nd}" matches "٥"  -- Arabic-Indic digit five
#guard "\\p{Nd}" matches "५"  -- Devanagari digit five

-- Script
#guard "\\p{Script=Greek}" matches "Α"
#guard "\\p{Script=Greek}" matches "ω"
#guard "\\p{Script=Greek}" doesn't match "A"

#guard "\\p{sc=Cyrillic}" matches "Ж"
#guard "\\p{sc=Arab}" matches "ع"
#guard "\\p{sc=Hani}" matches "中"

-- Script_Extensions
#guard "\\p{scx=Hira}" matches "ー"  -- Common script, but used with Hiragana

-- Binary properties
#guard "\\p{Alphabetic}" matches "A"
#guard "\\p{Alphabetic}" matches "α"
#guard "\\p{Alphabetic}" matches "中"
#guard "\\p{Alphabetic}" doesn't match "5"

#guard "\\p{White_Space}" matches " "
#guard "\\p{White_Space}" matches "\t"
#guard "\\p{White_Space}" matches "\u{2028}"  -- Line separator
#guard "\\p{White_Space}" doesn't match "a"

-- Core properties
#guard "\\p{Any}" matches any character
#guard "\\p{ASCII}" matches "A"
#guard "\\p{ASCII}" doesn't match "Σ"
#guard "\\p{Assigned}" doesn't match unassigned code points

-- Negation
#guard "\\P{ASCII}" doesn't match "A"
#guard "\\P{ASCII}" matches "Σ"
#guard "\\P{ASCII}" matches "中"

Edge Cases

-- Category unions (L includes Lu, Ll, Lt, Lm, Lo)
#guard "\\p{L}" matches "A"  -- Lu
#guard "\\p{L}" matches "a"  -- Ll
#guard "\\p{L}" matches "Dž"  -- Lt (titlecase)
#guard "\\p{L}" matches "ª"  -- Lm (modifier)
#guard "\\p{L}" matches "中" -- Lo (other)

-- Ranges with properties
#guard "[\\p{L}&&[A-Z]]" matches "A"  -- Letter AND A-Z
#guard "[\\p{Greek}--[α-ω]]" matches "Α"  -- Greek except lowercase

-- Multiple properties
#guard "[\\p{Lu}\\p{Ll}]" matches "A"
#guard "[\\p{Lu}\\p{Ll}]" matches "a"

-- Boundary cases
#guard "\\p{Lu}" doesn't match "\u{10FFFF}"  -- Last code point
#guard "\\p{ASCII}" matches "\u{7F}"  -- DEL
#guard "\\p{ASCII}" doesn't match "\u{80}"

-- Combining marks
#guard "\\p{Mn}" matches "\u{0301}"  -- Combining acute accent
#guard "e\\p{Mn}" matches "é"  -- e + combining acute

Corpus Tests

Enable Unicode tests in regex/tests/testdata/:

• unicode.toml - General Unicode tests
• flags.toml - Case-insensitive with Unicode
• Update others to use \p{...} where appropriate

Performance Tests

-- Ensure property checks are fast
-- Property lookups should use optimized tables (2-stage lookup)
-- Not linear search through all code points!

---

Implementation Strategy

Recommended Approach

Week 1: Investigation

• Research UnicodeBasic thoroughly
• Create decision document
• Set up testing framework

Week 2: Data structures

• Define types
• Basic scaffolding
• No parsing yet, just internal representation

Week 3: Parser

• Implement property syntax parsing
• Property name normalization
• Error handling

Weeks 4-5: Properties implementation

• Start with simple ones (Any, ASCII, Assigned)
• Then binary properties (Alphabetic, Uppercase, etc.)
• Then enumerated (General_Category, Script)
• Integration with UnicodeBasic or data tables

Week 6: Testing & proofs

• Comprehensive test suite
• Update correctness proofs with the properties support

Alternative if UnicodeBasic Incomplete

If UnicodeBasic doesn't provide all needed properties:

1. Contribute to UnicodeBasic: Add missing properties (preferred)
2. Custom implementation: Generate all tables from Unicode data files

Discuss with maintainers before choosing.

---

Resources

Unicode Data Files

• UnicodeData.txt: General_Category, character properties
• Scripts.txt: Script property
• ScriptExtensions.txt: Script_Extensions property
• DerivedCoreProperties.txt: Alphabetic, Uppercase, Lowercase, etc.
• PropList.txt: White_Space, Noncharacter_Code_Point, etc.

All available at: https://www.unicode.org/Public/UCD/latest/ucd/

Documentation

• UTS#18 Specification: UTS #18_ Unicode Regular Expressions.html (lines 1024-1531)
• Compliance Analysis: uts18_compliance_check.md (lines 137-327)
• UAX#44 (UCD): https://www.unicode.org/reports/tr44/
• UAX#24 (Script): https://www.unicode.org/reports/tr24/

Libraries

• UnicodeBasic: https://github.com/fgdorais/lean4-unicode-basic
• ICU (for reference): http://site.icu-project.org/

---

Notes for Contributors

Getting Started

1. Claim the issue: Leave a comment to show your interest
2. Start with investigation: Don't jump into coding - understand what's available first
3. Ask questions early: This is a large feature, discussion is encouraged
4. Incremental PRs: Consider breaking this into smaller PRs

Common Pitfalls

• ❌ Don't do linear search through all code points for each match
• ❌ Don't hardcode all Unicode data - use library or generated tables
• ❌ Don't forget property name aliases (both short and long forms)
• ❌ Don't forget case-insensitive property name matching
• ✅ Do optimize for common cases (ASCII, common properties)
• ✅ Do test with real Unicode text (Greek, Chinese, Arabic, emoji)

Questions?

This is a complex feature! Please don't hesitate to:

• Ask questions in this issue
• Discuss design decisions before implementing
• Request code review early and often

---

Related Issues

• Blocks: RL1.4 (Word Boundaries) - needs Alphabetic, Nd properties
• Blocks: RL1.5 (Case Insensitive) - needs case folding data
• Enables: Much better Unicode support throughout the engine
• After this: RL1.3 (Set Operations) works much better with \p{...}