Unicode RL1.1 support: Add \u{...} Hex Notation for Full Unicode Range (#149)

* Add support for \u{...} variable-length Unicode escape syntax

* Refactor Unicode escape parser for better code clarity

* Remove unused error variants from Parser.Error

* Fix formatting of hexNumberVariable parser

---------

Co-authored-by: pandaman <kointosudesuyo@infoseek.jp>

Author: yuuki14202028

regex/Regex/Syntax/Parser/Basic.lean

@@ -42,7 +42,7 @@ def specialCharacters := "[](){*+?|^$.\\"
 
 def escapedChar : Parser.LT s Error (Char ⊕ PerlClass) :=
   charOrError '\\' *>
-    ((Sum.inl <$> (simple <|> hex2 <|> hex4)) <|> (Sum.inr <$> perlClass)).commit
+    ((Sum.inl <$> (simple <|> hexEscape)) <|> (Sum.inr <$> perlClass)).commit
 where
   simple : Parser.LT s Error Char :=
     anyCharOrError
@@ -62,11 +62,22 @@ where
           pure c
         else
           throw (.unexpectedEscapedChar c)
-  hex2 : Parser.LT s Error Char :=
-    charOrError 'x' *> (Char.ofNat <$> hexNumberN 2).commit
-  -- TODO: support "\u{XXXX}" and "\u{XXXXX}"
-  hex4 : Parser.LT s Error Char :=
-    charOrError 'u' *> (Char.ofNat <$> hexNumberN 4).commit
+  hexEscape : Parser.LT s Error Char :=
+    (charOrError 'x' *> (Char.ofNat <$> hexNumberN 2).commit)
+    <|> (charOrError 'u' *> unicodeEscape.commit)
+  unicodeEscape : Parser.LT s Error Char :=
+    hexNumberVariable.guard fun n =>
+      if n.isValidChar then .ok (Char.ofNat n)
+      else .error (.invalidCodePoint n)
+  hexNumberVariable : Parser.LT s Error Nat :=
+    betweenOr (charOrError '{') (charOrError '}').commit (.commit do
+      let digits ← (many1 hexDigit).weaken
+      if digits.size > 6 then
+        throw (.tooManyHexDigits digits.size)
+      else
+        pure (digits.foldl (fun n d => 16 * n + d) 0)
+    )
+    <|> hexNumberN 4
   perlClass : Parser.LT s Error PerlClass :=
     anyCharOrError
     |>.guard fun c =>

regex/Regex/Syntax/Parser/Error.lean

@@ -14,6 +14,8 @@ inductive Error where
   | invalidRange (c₁ : Char) (c₂ : Char)
   | invalidRepetition (min : Nat) (max : Nat)
   | expectedEof
+  | invalidCodePoint (n : Nat)
+  | tooManyHexDigits (n : Nat)
 deriving Repr, Inhabited, DecidableEq
 
 instance : ToString Error where
@@ -26,5 +28,7 @@ instance : ToString Error where
     | .invalidRange c₁ c₂ => s!"invalid range: {c₁}..{c₂}"
     | .invalidRepetition min max => s!"invalid repetition: {min}..{max}"
     | .expectedEof => "expected EOF"
+    | .invalidCodePoint n => s!"invalid code point: 0x{n.toDigits 16}"
+    | .tooManyHexDigits n => s!"too many hex digits: {n}"
 
 end Regex.Syntax.Parser

regex/Regex/Syntax/Parser/Test.lean

@@ -127,8 +127,6 @@ private def test (input : String) (expected : Ast) : Bool :=
 #guard parseAst "\\x" = .error .unexpectedEof
 #guard parseAst "\\u" = .error .unexpectedEof
 #guard parseAst "\\u12" = .error .unexpectedEof
-#guard parseAst "\\u{}" = .error (.unexpectedChar '{')
-#guard parseAst "\\u{xyz}" = .error (.unexpectedChar '{')
 #guard parseAst "[]" = .error (.unexpectedChar ']')
 #guard parseAst "[^]" = .error (.unexpectedChar ']')
 #guard parseAst "a{1" = .error .unexpectedEof
@@ -140,7 +138,61 @@ private def test (input : String) (expected : Ast) : Bool :=
 #guard parseAst "(?:a" = .error .unexpectedEof
 #guard parseAst "(?:" = .error .unexpectedEof
 
--- We do not support \u{...} yet.
-#guard parseAst "\\u{1234}" = .error (.unexpectedChar '{')
+-- 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))
+
+-- 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 (.unexpectedChar 'G')
+#guard parseAst "\\u{12.34}" = .error (.unexpectedChar '.')
+
+-- Missing closing brace
+#guard parseAst "\\u{1234" = .error (.unexpectedEof)
+
+-- 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)
 
 end Regex.Syntax.Parser.Test