Unicode RL1.1 support: Add `\u{...}` Hex Notation for Full Unicode Range

[pandaman64]

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

Difficulty: Beginner to Intermediate
UTS#18 Requirement: RL1.1 Hex Notation

Summary

Current Status

🟡 40/100 - Partial Implementation

The regex parser currently supports:

• \xXX - 2-digit hex (U+0000 to U+00FF) - 256 characters
• \uXXXX - 4-digit hex (U+0000 to U+FFFF) - BMP only

Coverage: Only 5.9% of Unicode (65,536 of 1,114,112 code points)

UTS#18 Requirement

RL1.1 Hex Notation: To meet this requirement, an implementation shall supply a mechanism for specifying any Unicode code point (from U+0000 to U+10FFFF), using the hexadecimal code point representation.

The syntax must use the code point in hexadecimal form. For example: \u{1D11E}, \x{1D11E}.

Goals

Add \u{...} syntax to support the full Unicode range (U+0000 to U+10FFFF), enabling:

• ✅ Emoji support (U+1F300-U+1F9FF): \u{1F600} for 😀
• ✅ Supplementary plane characters (U+10000-U+10FFFF)
• ✅ Ancient scripts, mathematical symbols, additional CJK ideographs

Acceptance Criteria

• Parser accepts \u{...} syntax with 1-6 hex digits
• Supports full range U+0000 to U+10FFFF
• Rejects invalid code points > U+10FFFF with clear error message
• Handles supplementary plane characters correctly (U+10000-U+10FFFF)
• All existing \xXX and \uXXXX tests still pass
• New tests cover emoji, edge cases, and error conditions

---

Technical Details

Current Implementation

Location: regex/Regex/Syntax/Parser/Basic.lean:63-67

The parser already has a TODO comment for this feature:

-- TODO: support "\u{XXXX}" and "\u{XXXXX}"

Current hex parsers:

def hexNumber2 : Parser.LT Error Nat := ...  -- \xXX
def hexNumber4 : Parser.LT Error Nat := ...  -- \uXXXX

Test Evidence (regex/Regex/Syntax/Parser/Test.lean:143-144):

-- We do not support \u{...} yet.
#guard parseAst "\\u{1234}" = .error (.unexpectedChar '{')

What Needs to Change

1. Add Variable-Length Hex Parser

Create a new parser that accepts 1-6 hex digits:

-- regex/Regex/Syntax/Parser/Basic.lean
def hexNumberVariable : Parser.LT Error Nat :=
  -- Parse 1 to 6 hex digits
  -- Convert to Nat
  -- Return the value

Key points:

• Must accept 1-6 hex digits
• Valid range: 0x0 to 0x10FFFF
• Examples: \u{0}, \u{7F}, \u{10000}, \u{10FFFF}

Note: The valid Unicode range is U+0000 to U+10FFFF, which is 0x10FFFF = 1,114,111. This requires up to 6 hex digits (not 5).

2. Add Validation

After parsing the hex value, validate it:

if n > 0x10FFFF then
  -- Return error: code point too large
else if n >= 0xD800 && n <= 0xDFFF then
  -- Optional: reject surrogates
  -- Lean's Char type may already handle this
else
  -- Valid code point
  return Char.ofNat n

3. Update Parser Integration

Add the new syntax to the escape sequence parser:

def escapedChar : Parser.LT Error Char :=
  charOrError '\\' *>
    (hexEscape <|> namedEscape <|> singleCharEscape)
where
  hexEscape : Parser.LT Error Char :=
    (charOrError 'x' *> hexNumber2).map Char.ofNat
    <|> (charOrError 'u' *> hexDigits).map Char.ofNat
  
  hexDigits : Parser.LT Error Nat :=
    (charOrError '{' *> hexNumberVariable <* charOrError '}')
    <|> hexNumber4

4. Key Files to Modify

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

   • Add hexNumberVariable function
   • Integrate into escapedChar parser
   • Add validation logic

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

   • Add new error variant: invalidCodePoint : Nat → Error

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

   • Update existing test (line 143-144)
   • Add comprehensive test suite

Implementation Approach

Step 1: Add the hex parser

def hexNumberVariable : Parser.LT Error Nat := do
  sorry

Step 2: Add validation

def validateCodePoint (n : Nat) : Except Error Char := do
  if n > 0x10FFFF then
    .error (.invalidCodePoint n)
  else
    -- Check if Char.ofNat handles surrogates correctly
    .ok (Char.ofNat n)

Step 3: Integrate and test

• Update parser to use new function
• Run existing tests to ensure no regression
• Add new tests (see below)

---

Testing

Test Cases

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

Valid Cases

-- Minimum
#guard parseAst "\\u{0}" = .ok (.char '\x00')

-- ASCII range
#guard parseAst "\\u{7F}" = .ok (.char '\x7F')
#guard parseAst "\\u{41}" = .ok (.char 'A')

-- Latin-1 Supplement
#guard parseAst "\\u{80}" = .ok (.char (Char.ofNat 0x80))
#guard parseAst "\\u{FF}" = .ok (.char 'ÿ')

-- BMP (Basic Multilingual Plane)
#guard parseAst "\\u{1234}" = .ok (.char (Char.ofNat 0x1234))
#guard parseAst "\\u{FFFF}" = .ok (.char (Char.ofNat 0xFFFF))

-- Supplementary planes (emoji and beyond)
#guard parseAst "\\u{10000}" = .ok (.char (Char.ofNat 0x10000))
#guard parseAst "\\u{1F600}" = .ok (.char '😀')  -- GRINNING FACE
#guard parseAst "\\u{1F4A9}" = .ok (.char '💩')  -- PILE OF POO
#guard parseAst "\\u{1F47D}" = .ok (.char '👽')  -- EXTRATERRESTRIAL ALIEN

-- Maximum valid code point
#guard parseAst "\\u{10FFFF}" = .ok (.char (Char.ofNat 0x10FFFF))

-- Lowercase hex digits
#guard parseAst "\\u{1f600}" = .ok (.char '😀')
#guard parseAst "\\u{abcd}" = .ok (.char (Char.ofNat 0xABCD))

-- Variable length (1-6 digits)
#guard parseAst "\\u{a}" = .ok (.char (Char.ofNat 0xA))
#guard parseAst "\\u{AB}" = .ok (.char (Char.ofNat 0xAB))
#guard parseAst "\\u{ABC}" = .ok (.char (Char.ofNat 0xABC))
#guard parseAst "\\u{ABCD}" = .ok (.char (Char.ofNat 0xABCD))
#guard parseAst "\\u{ABCDE}" = .ok (.char (Char.ofNat 0xABCDE))

Error Cases

-- Empty braces
#guard parseAst "\\u{}" = .error (.unexpectedChar '}')

-- Too large (beyond Unicode)
#guard parseAst "\\u{110000}" = .error (.invalidCodePoint 0x110000)
#guard parseAst "\\u{FFFFFF}" = .error (.invalidCodePoint 0xFFFFFF)

-- Too many digits (>6)
#guard parseAst "\\u{1234567}" = .error (.tooManyHexDigits 7)

-- Invalid hex characters
#guard parseAst "\\u{GHIJ}" = .error (.invalidHexChar 'G')
#guard parseAst "\\u{12.34}" = .error (.invalidHexChar '.')

-- Missing closing brace
#guard parseAst "\\u{1234" = .error (.unexpectedEndOfInput)

-- Surrogate range (optional, depending on Lean's Char behavior)
-- If Lean's Char.ofNat rejects surrogates, these should error:
#guard parseAst "\\u{D800}" = .error (.invalidCodePoint 0xD800)
#guard parseAst "\\u{DFFF}" = .error (.invalidCodePoint 0xDFFF)

Edge Cases to Cover

1. Boundary values:

   • \u{0} - minimum
   • \u{10FFFF} - maximum valid
   • \u{110000} - first invalid

2. Case sensitivity:

   • Both \u{1F600} and \u{1f600} should work
   • Mix: \u{1F6aB}

3. Leading zeros:

   • \u{0000} should equal \u{0}
   • \u{001234} should equal \u{1234}

4. Unicode planes:

   • BMP: \u{0}-\u{FFFF}
   • SMP: \u{10000}-\u{1FFFF} (Supplementary Multilingual Plane)
   • SIP: \u{20000}-\u{2FFFF} (Supplementary Ideographic Plane)
   • TIP: \u{30000}-\u{3FFFF} (Tertiary Ideographic Plane)
   • Planes 4-13: \u{40000}-\u{DFFFF}
   • SSP: \u{E0000}-\u{EFFFF} (Supplementary Special-purpose Plane)
   • PUA-A/B: \u{F0000}-\u{10FFFF} (Private Use Areas)

5. Integration:

   • \u{1F600}+ - with quantifiers
   • [\u{1F300}-\u{1F5FF}] - in ranges
   • \u{41}\u{301} - combining sequences (A + combining acute = Á)

Corpus Tests

Verify against existing test suite in regex/tests/testdata/:

• Ensure emoji tests pass
• Check that patterns with supplementary characters work

---

Resources

• UTS#18 Specification: UTS #18_ Unicode Regular Expressions.html (lines 796-892)
• Compliance Analysis: uts18_compliance_check.md (lines 50-136)
• Current Parser: regex/Regex/Syntax/Parser/Basic.lean
• Unicode Code Charts: https://www.unicode.org/charts/

Questions?

If you have questions while implementing this, please comment on this issue!

Related Issues

• After this is implemented, RL1.7 (Code Points) will be 100% complete
• This enables better emoji support throughout the regex engine

[yuuki14202028]

After reading your blog, I tried implementing it. I've created a draft PR for your review.
Since I don't speak English myself, I had this written by an AI.

[pandaman64]

こんにちは！コントリビューションありがとうございます！
PRは追々確認しますが、諸々の連絡には https://x.com/yuuki14202028 にメッセージを送ればよいでしょうか。

[yuuki14202028]

はい。それで大丈夫です。

[pandaman64]

Fixed by #149