Unicode RL1.3 support: Add Set Operations in Character Classes (&&, --, ||, ~~) #138

regex/Regex/Data/Classes.lean

@@ -40,16 +40,28 @@ def Class.mem (c : Char) : Class → Bool
   | Class.range s e => s ≤ c ∧ c ≤ e
   | Class.perl pc => pc.mem c
 
-structure Classes where
-  negated : Bool
-  classes : Array Class
+-- Algebraic data type for set operations
+inductive Classes where
+  | atom : Class → Classes
+  | complement : Classes → Classes
+  | union : Classes → Classes → Classes
+  | intersection : Classes → Classes → Classes
+  | difference : Classes → Classes → Classes
+  | symDiff : Classes → Classes → Classes
 deriving Repr, DecidableEq, Inhabited, Lean.ToExpr
 
-def Classes.mem (c : Char) (cs : Classes) : Bool :=
-  if cs.negated then
-    cs.classes.all (fun cls => !cls.mem c)
-  else
-    cs.classes.any (fun cls => cls.mem c)
+-- Evaluation
+def Classes.mem (c : Char) (e : Classes) : Bool :=
+  match e with
+  | .atom cls => cls.mem c
+  | .complement e' => !e'.mem c
+  | .union e1 e2 => e1.mem c || e2.mem c
+  | .intersection e1 e2 => e1.mem c && e2.mem c
+  | .difference e1 e2 => e1.mem c && !e2.mem c
+  | .symDiff e1 e2 =>
+      let m1 := e1.mem c
+      let m2 := e2.mem c
+      (m1 || m2) && !(m1 && m2)
 
 instance : Membership Char Classes where
   mem cs c := cs.mem c

regex/Regex/Syntax/Ast.lean

@@ -65,8 +65,8 @@ def Ast.toRegexAux (index : Nat) (ast : Ast) : Nat × Expr :=
     let (index', r) := h.toRegexAux index
     (index', applyRepetitions min max greedy r)
   | .classes cs => (index, .classes cs)
-  | .perl pc => (index, .classes ⟨false, #[Class.perl pc]⟩)
-  | .dot => (index, .classes ⟨false, #[Class.beforeLineBreak, Class.afterLineBreak]⟩)
+  | .perl pc => (index, .classes (Classes.atom (Class.perl pc)))
+  | .dot => (index, .classes (.union (Classes.atom Class.beforeLineBreak) (Classes.atom Class.afterLineBreak)))
 
 def Ast.toRegex (ast : Ast) : Expr := (ast.toRegexAux 0).2
 

regex/Regex/Syntax/Parser/Basic.lean

@@ -111,7 +111,7 @@ def dot : Parser.LT s Error Ast :=
 
 def charInClass : Parser.LT s Error (Char ⊕ PerlClass) :=
   escapedChar <|> (anyCharOrError.guard fun c =>
-    if c = ']' ∨ c = '\\' then throw (.unexpectedChar c)
+    if c = '[' ∨ c = ']' ∨ c = '\\' then throw (.unexpectedChar c)
     else .ok (.inl c)
   )
 
@@ -138,12 +138,69 @@ where
     | .inl c => .single c
     | .inr cls => .perl cls
 
-def classes : Parser.LT s Error Ast :=
-  betweenOr (charOrError '[') (charOrError ']').commit (.commit do
-    let negated ← test '^'
-    let classes ← (many1 singleClass).weaken
-    pure (Ast.classes ⟨negated, classes⟩)
+def classesAtom : Parser.LT s Error Classes :=
+  singleClass.map Classes.atom
+
+def classesOperator : Parser.LT s Error (Classes → Classes → Classes) :=
+    (charOrError '-' *> charOrError '-' |>.mapConst Classes.difference)
+    <|> (charOrError '&' *> charOrError '&' |>.mapConst Classes.intersection)
+    <|> (charOrError '|' *> charOrError '|' |>.mapConst Classes.union)
+    <|> (charOrError '~' *> charOrError '~' |>.mapConst Classes.symDiff)
+
+mutual
+
+def characterClasses (pos : Pos s) : Result.LT pos Error Classes :=
+  charOrError '[' pos
+  |>.bind' (fun _ pos₁ h₁ => .commit $
+    ((charOrError ':' pos₁).bind (fun _ =>
+      (Result.fatal Error.unsupportedCharacterClass : Result.LT _ Error Classes)))
+    <|>
+    (test '^' pos₁).bind' (fun complement pos₂ h₂ =>
+      have : Rel.LT pos₂ pos := Trans.trans h₂ h₁
+      (classesSeq pos₂).map (fun classes =>
+        if complement then
+          classes.complement
+        else
+          classes
+      )
+    )
   )
+  |>.bind' fun classes pos₃ _ =>
+    (charOrError ']' pos₃).commit.map fun _ => classes
+termination_by (pos, 10)
+
+def classesItem (pos : Pos s) : Result.LT pos Error Classes :=
+  classesAtom pos <|> characterClasses pos
+termination_by (pos, 20)
+
+def classesSeq1 (acc : Classes) (pos : Pos s) : Result.LE pos Error Classes :=
+  (classesOperator pos
+  |>.bind' fun op pos₁ h =>
+    (characterClasses pos₁).commit
+    |>.bind' fun right pos₂ h2 =>
+      have : Rel.LT pos₂ pos := Trans.trans h2 h
+      classesSeq1 (op acc right) pos₂
+  ).weaken
+  <|>
+  (classesItem pos
+  |>.bind' fun right pos₁ _ =>
+    classesSeq1 (Classes.union acc right) pos₁
+  ).weaken
+  <|>
+  pure acc
+termination_by (pos, 30)
+
+def classesSeq (pos : Pos s) : Result.LE pos Error Classes :=
+  (classesItem pos
+  |>.bind' fun first pos₁ _ =>
+    classesSeq1 first pos₁
+  ).weaken.commit
+termination_by (pos, 40)
+
+end
+
+def classes : Parser.LT s Error Ast :=
+  fun pos => (characterClasses pos).map Ast.classes
 
 def repetitionInner : Parser.LT s Error (Nat × Option Nat) :=
   (charOrError '*' |>.mapConst (0, .none))

regex/Regex/Syntax/Parser/Error.lean

@@ -16,6 +16,7 @@ inductive Error where
   | expectedEof
   | invalidCodePoint (n : Nat)
   | tooManyHexDigits (n : Nat)
+  | unsupportedCharacterClass
 deriving Repr, Inhabited, DecidableEq
 
 instance : ToString Error where
@@ -30,5 +31,6 @@ instance : ToString Error where
     | .expectedEof => "expected EOF"
     | .invalidCodePoint n => s!"invalid code point: 0x{n.toDigits 16}"
     | .tooManyHexDigits n => s!"too many hex digits: {n}"
+    | .unsupportedCharacterClass => "unsupported character class"
 
 end Regex.Syntax.Parser

regex/Regex/Syntax/Parser/Test.lean

@@ -33,17 +33,59 @@ private def test (input : String) (expected : Ast) : Bool :=
 #guard test "$" (.anchor .eos)
 #guard test "^abc$" (.concat (.concat (.concat (.concat (.anchor .start) (.char 'a')) (.char 'b')) (.char 'c')) (.anchor .eos))
 
-#guard test "[abc]" (.classes ⟨false, #[.single 'a', .single 'b', .single 'c']⟩)
-#guard test "[^abc]" (.classes ⟨true, #[.single 'a', .single 'b', .single 'c']⟩)
-#guard test "[a-z]" (.classes ⟨false, #[.range 'a' 'z']⟩)
-#guard test r"[\da]" (.classes ⟨false, #[.perl ⟨false, .digit⟩, .single 'a']⟩)
-#guard test "[-]" (.classes ⟨false, #[.single '-']⟩)
-#guard test "[a-]" (.classes ⟨false, #[.single 'a', .single '-']⟩)
+#guard test "[abc]" (.classes (.union (.union (.atom (.single 'a')) (.atom (.single 'b'))) (.atom (.single 'c'))))
+#guard test "[^abc]" (.classes (.complement (.union (.union (.atom (.single 'a')) (.atom (.single 'b'))) (.atom (.single 'c')))))
+#guard test "[a-z]" (.classes (.atom (.range 'a' 'z')))
+#guard test r"[\da]" (.classes (.union (.atom (.perl ⟨false, .digit⟩)) (.atom (.single 'a'))))
+#guard test "[-]" (.classes (.atom (.single '-')))
+#guard test "[a-]" (.classes (.union (.atom (.single 'a')) (.atom (.single '-'))))
 -- special characters are allowed in classes
-#guard test r"[(){}*+?|^$.\--]" (.classes ⟨false, #[
-  '(', ')', '{', '}', '*', '+', '?', '|', '^', '$', '.', '-', '-'
-].map .single⟩)
-
+#guard test r"[(){}*+?|^$.\--]" (
+  .classes ("){}*+?|^$.--".foldl (fun acc c => .union acc (.atom (.single c))) (.atom (.single '(')))
+)
+#guard test "[[a]--[b]]" (.classes (.difference (.atom (.single 'a')) (.atom (.single 'b'))))
+#guard test "[[a]&&[b]]" (.classes (.intersection (.atom (.single 'a')) (.atom (.single 'b'))))
+#guard test "[[a]||[b]]" (.classes (.union (.atom (.single 'a')) (.atom (.single 'b'))))
+#guard test "[[^a]--[b]]" (.classes (.difference (.complement (.atom (.single 'a'))) (.atom (.single 'b'))))
+#guard test "[[a]--[^b]]" (.classes (.difference (.atom (.single 'a')) (.complement (.atom (.single 'b')))))
+#guard test "[[^a]--[^b]]" (.classes (.difference (.complement (.atom (.single 'a'))) (.complement (.atom (.single 'b')))))
+#guard parseAst "[a--b]" = .error (.unexpectedChar 'b')
+#guard parseAst "[^a--b]" = .error (.unexpectedChar 'b')
+#guard parseAst "[a--^b]" = .error (.unexpectedChar '^')
+#guard parseAst "[a&&b]" = .error (.unexpectedChar 'b')
+#guard test "[[a-zA-Z]--[aeiouAEIOU]]" (.classes
+  (.difference
+    (.union
+      (.atom (.range 'a' 'z'))
+      (.atom (.range 'A' 'Z')))
+    ("eiouAEIOU".foldl (fun acc c => .union acc (.atom (.single c))) (.atom (.single 'a')))))
+#guard parseAst "[:.]" = .error .unsupportedCharacterClass
+#guard parseAst "[.:]" = .ok (.classes (.union (.atom (.single '.')) (.atom (.single ':'))))
+#guard test "[a-z&&[^aeiou]]" (.classes
+  (.intersection
+    (.atom (.range 'a' 'z'))
+    (.complement
+      ("eiou".foldl (fun acc c => .union acc (.atom (.single c))) (.atom (.single 'a'))))))
+#guard test "[[a]&&[b]||[c]--[d]~~[e]]" (.classes
+  (.symDiff
+    (.difference
+      (.union
+        (.intersection
+          (.atom (.single 'a'))
+          (.atom (.single 'b')))
+        (.atom (.single 'c')))
+      (.atom (.single 'd')))
+    (.atom (.single 'e'))))
+#guard test "[[a]&&[[b]||[c]]--[[d]~~[e]]]" (.classes
+  (.difference
+    (.intersection
+      (.atom (.single 'a'))
+      (.union
+        (.atom (.single 'b'))
+        (.atom (.single 'c'))))
+    (.symDiff
+      (.atom (.single 'd'))
+      (.atom (.single 'e')))))
 #guard test "|" (.alternate .epsilon .epsilon)
 #guard test "a|" (.alternate (.char 'a') .epsilon)
 #guard test "|a" (.alternate .epsilon (.char 'a'))

regex/tests/CorpusTest-backtracker.csv

@@ -60,12 +60,12 @@ crazy/start-end-empty-rep,ok,
 crazy/start-end-empty-rep-rev,ok,
 crazy/neg-class-letter,ok,
 crazy/neg-class-letter-comma,ok,
-crazy/neg-class-letter-space,error,"expected '[^a[:space:]]' to compile, but it did not: expected EOF"
+crazy/neg-class-letter-space,error,"expected '[^a[:space:]]' to compile, but it did not: unsupported character class"
 crazy/neg-class-comma,ok,
-crazy/neg-class-space,error,"expected '[^[:space:]]' to compile, but it did not: expected EOF"
-crazy/neg-class-space-comma,error,"expected '[^,[:space:]]' to compile, but it did not: expected EOF"
-crazy/neg-class-comma-space,error,"expected '[^[:space:],]' to compile, but it did not: expected EOF"
-crazy/neg-class-ascii,error,"expected '[^[:alpha:]Z]' to compile, but it did not: expected EOF"
+crazy/neg-class-space,error,"expected '[^[:space:]]' to compile, but it did not: unsupported character class"
+crazy/neg-class-space-comma,error,"expected '[^,[:space:]]' to compile, but it did not: unsupported character class"
+crazy/neg-class-comma-space,error,"expected '[^[:space:],]' to compile, but it did not: unsupported character class"
+crazy/neg-class-ascii,error,"expected '[^[:alpha:]Z]' to compile, but it did not: unsupported character class"
 crazy/lazy-many-many,ok,
 crazy/lazy-many-optional,ok,
 crazy/lazy-one-many-many,ok,
@@ -398,7 +398,7 @@ regression/unsorted-binary-search-200,error,"expected '(?i-u)[A_]+' to compile,
 regression/unicode-case-lower-nocase-flag,error,"expected '(?i)\p{Ll}+' to compile, but it did not: unexpected character: ?"
 regression/negated-char-class-100,error,"expected '(?i)[^x]' to compile, but it did not: unexpected character: ?"
 regression/negated-char-class-200,error,"expected '(?i)[^x]' to compile, but it did not: unexpected character: ?"
-regression/ascii-word-underscore,error,"expected '[[:word:]]' to compile, but it did not: expected EOF"
+regression/ascii-word-underscore,error,"expected '[[:word:]]' to compile, but it did not: unsupported character class"
 regression/captures-repeat,error,"expected '([a-f]){2}(?P<foo>[x-z])' to compile, but it did not: unexpected character: ?"
 regression/alt-in-alt-100,error,"expected #[{ id := 0, spans := #[some { start := 0, end := 1 }] }, { id := 0, spans := #[some { start := 2, end := 2 }] }], got #[#[(some (0, 1))], #[(some (2, 2))], #[(some (2, 2))]]"
 regression/alt-in-alt-200,ok,
@@ -441,8 +441,8 @@ regression/stops,unsupported,
 regression/stops-ascii,unsupported,
 regression/adjacent-line-boundary-100,error,"expected '(?m)^(?:[^ ]+?)$' to compile, but it did not: unexpected character: ?"
 regression/adjacent-line-boundary-200,error,"expected '(?m)^(?:[^ ]+?)$' to compile, but it did not: unexpected character: ?"
-regression/anchored-prefix-100,error,"expected '^a[[:^space:]]' to compile, but it did not: expected EOF"
-regression/anchored-prefix-200,error,"expected '^a[[:^space:]]' to compile, but it did not: expected EOF"
+regression/anchored-prefix-100,error,"expected '^a[[:^space:]]' to compile, but it did not: unsupported character class"
+regression/anchored-prefix-200,error,"expected '^a[[:^space:]]' to compile, but it did not: unsupported character class"
 regression/anchored-prefix-300,ok,
 regression/aho-corasick-100,ok,
 regression/interior-anchor-capture,ok,
@@ -469,11 +469,11 @@ regression/captures-wrong-order,ok,
 regression/negated-unicode-word-boundary-dfa-fail,error,"expected #[{ id := 0, spans := #[some { start := 0, end := 3 }] }], got #[#[(some (0, 3))], #[(some (3, 3))]]"
 regression/missed-match,ok,
 regression/regex-to-glob,unsupported,
-regression/reverse-inner-plus-shorter-than-expected,ok,
+regression/reverse-inner-plus-shorter-than-expected,error,"expected '(?:(\d+)[:.])?(\d{1,2})[:.](\d{2})' to compile, but it did not: unsupported character class"
 regression/reverse-inner-short,ok,
 regression/prefilter-with-aho-corasick-standard-semantics,unsupported,
 regression/non-prefix-literal-quit-state,ok,
-regression/hir-optimization-out-of-order-class,error,"expected '^[[:alnum:]./-]+$' to compile, but it did not: expected EOF"
+regression/hir-optimization-out-of-order-class,error,"expected '^[[:alnum:]./-]+$' to compile, but it did not: unsupported character class"
 regression/improper-reverse-suffix-optimization,ok,
 set/basic10,unsupported,
 set/basic10-leftmost-first,unsupported,

regex/tests/CorpusTest.csv

@@ -60,12 +60,12 @@ crazy/start-end-empty-rep,ok,
 crazy/start-end-empty-rep-rev,ok,
 crazy/neg-class-letter,ok,
 crazy/neg-class-letter-comma,ok,
-crazy/neg-class-letter-space,error,"expected '[^a[:space:]]' to compile, but it did not: expected EOF"
+crazy/neg-class-letter-space,error,"expected '[^a[:space:]]' to compile, but it did not: unsupported character class"
 crazy/neg-class-comma,ok,
-crazy/neg-class-space,error,"expected '[^[:space:]]' to compile, but it did not: expected EOF"
-crazy/neg-class-space-comma,error,"expected '[^,[:space:]]' to compile, but it did not: expected EOF"
-crazy/neg-class-comma-space,error,"expected '[^[:space:],]' to compile, but it did not: expected EOF"
-crazy/neg-class-ascii,error,"expected '[^[:alpha:]Z]' to compile, but it did not: expected EOF"
+crazy/neg-class-space,error,"expected '[^[:space:]]' to compile, but it did not: unsupported character class"
+crazy/neg-class-space-comma,error,"expected '[^,[:space:]]' to compile, but it did not: unsupported character class"
+crazy/neg-class-comma-space,error,"expected '[^[:space:],]' to compile, but it did not: unsupported character class"
+crazy/neg-class-ascii,error,"expected '[^[:alpha:]Z]' to compile, but it did not: unsupported character class"
 crazy/lazy-many-many,ok,
 crazy/lazy-many-optional,ok,
 crazy/lazy-one-many-many,ok,
@@ -398,7 +398,7 @@ regression/unsorted-binary-search-200,error,"expected '(?i-u)[A_]+' to compile,
 regression/unicode-case-lower-nocase-flag,error,"expected '(?i)\p{Ll}+' to compile, but it did not: unexpected character: ?"
 regression/negated-char-class-100,error,"expected '(?i)[^x]' to compile, but it did not: unexpected character: ?"
 regression/negated-char-class-200,error,"expected '(?i)[^x]' to compile, but it did not: unexpected character: ?"
-regression/ascii-word-underscore,error,"expected '[[:word:]]' to compile, but it did not: expected EOF"
+regression/ascii-word-underscore,error,"expected '[[:word:]]' to compile, but it did not: unsupported character class"
 regression/captures-repeat,error,"expected '([a-f]){2}(?P<foo>[x-z])' to compile, but it did not: unexpected character: ?"
 regression/alt-in-alt-100,error,"expected #[{ id := 0, spans := #[some { start := 0, end := 1 }] }, { id := 0, spans := #[some { start := 2, end := 2 }] }], got #[#[(some (0, 1))], #[(some (2, 2))], #[(some (2, 2))]]"
 regression/alt-in-alt-200,ok,
@@ -441,8 +441,8 @@ regression/stops,unsupported,
 regression/stops-ascii,unsupported,
 regression/adjacent-line-boundary-100,error,"expected '(?m)^(?:[^ ]+?)$' to compile, but it did not: unexpected character: ?"
 regression/adjacent-line-boundary-200,error,"expected '(?m)^(?:[^ ]+?)$' to compile, but it did not: unexpected character: ?"
-regression/anchored-prefix-100,error,"expected '^a[[:^space:]]' to compile, but it did not: expected EOF"
-regression/anchored-prefix-200,error,"expected '^a[[:^space:]]' to compile, but it did not: expected EOF"
+regression/anchored-prefix-100,error,"expected '^a[[:^space:]]' to compile, but it did not: unsupported character class"
+regression/anchored-prefix-200,error,"expected '^a[[:^space:]]' to compile, but it did not: unsupported character class"
 regression/anchored-prefix-300,ok,
 regression/aho-corasick-100,ok,
 regression/interior-anchor-capture,ok,
@@ -469,11 +469,11 @@ regression/captures-wrong-order,ok,
 regression/negated-unicode-word-boundary-dfa-fail,error,"expected #[{ id := 0, spans := #[some { start := 0, end := 3 }] }], got #[#[(some (0, 3))], #[(some (3, 3))]]"
 regression/missed-match,ok,
 regression/regex-to-glob,unsupported,
-regression/reverse-inner-plus-shorter-than-expected,ok,
+regression/reverse-inner-plus-shorter-than-expected,error,"expected '(?:(\d+)[:.])?(\d{1,2})[:.](\d{2})' to compile, but it did not: unsupported character class"
 regression/reverse-inner-short,ok,
 regression/prefilter-with-aho-corasick-standard-semantics,unsupported,
 regression/non-prefix-literal-quit-state,ok,
-regression/hir-optimization-out-of-order-class,error,"expected '^[[:alnum:]./-]+$' to compile, but it did not: expected EOF"
+regression/hir-optimization-out-of-order-class,error,"expected '^[[:alnum:]./-]+$' to compile, but it did not: unsupported character class"
 regression/improper-reverse-suffix-optimization,ok,
 set/basic10,unsupported,
 set/basic10-leftmost-first,unsupported,