update Cegex to using matched operator for capturing instead of group operator

Author: awalterschulze

Validator/Learning/Cegex/Cegex.lean

@@ -2,24 +2,26 @@
 inductive Cegex where
   | emptyset
   | epsilon
+  | matched (c: Char)
   | char (c: Char)
   | or (y z: Cegex)
   | concat (y z: Cegex)
   | star (y: Cegex)
   -- group is the only new operator compared to a Cegex without capturing groups.
-  | group (id: Nat) (capture: List Char) (x: Cegex)
+  | group (id: Nat) (x: Cegex)
   deriving DecidableEq, Ord, Repr, Hashable
 
 def Cegex.nullable (x: Cegex): Bool :=
   match x with
   | Cegex.emptyset => false
   | Cegex.epsilon => true
+  | Cegex.matched _ => true
   | Cegex.char _ => false
   | Cegex.or y z => nullable y || nullable z
   | Cegex.concat y z => nullable y && nullable z
   | Cegex.star _ => true
   -- The group is nullable if its embedded expression is nullable.
-  | Cegex.group _ _ y => nullable y
+  | Cegex.group _ y => nullable y
 
 def Cegex.unescapable (x: Cegex): Bool :=
   match x with

Validator/Learning/Cegex/CegexCapture.lean

@@ -1,6 +1,6 @@
--- This algorithm is from Regular Expression Sub-Matching using Partial Derivatives - Martin Sulzmann and Kenny Zhuo Ming Lu
+-- Based on algorithm from Regular Expression Sub-Matching using Partial Derivatives - Martin Sulzmann and Kenny Zhuo Ming Lu
+-- Thank you Keegan Perry for simplifying and explaining the original to me.
 
--- Thank you Keegan Perry for simplifying and explaining this to me.
 import Validator.Learning.Cegex.Cegex
 
 namespace CegexCapture
@@ -12,19 +12,21 @@ def neutralize (x: Cegex): Cegex :=
   match x with
   | Cegex.emptyset => Cegex.emptyset
   | Cegex.epsilon => Cegex.epsilon
+  | Cegex.matched c => Cegex.matched c
   | Cegex.char _ => Cegex.emptyset
   | Cegex.or y z => Cegex.smartOr (neutralize y) (neutralize z)
   | Cegex.concat y z => Cegex.concat (neutralize y) (neutralize z)
   | Cegex.star y => Cegex.star (neutralize y)
-  | Cegex.group id c y => Cegex.group id c (neutralize y)
+  | Cegex.group id y => Cegex.group id (neutralize y)
 
 partial def derive (x: Cegex) (char: Char): Cegex :=
   match x with
   | Cegex.emptyset => Cegex.emptyset
   | Cegex.epsilon => Cegex.emptyset
+  | Cegex.matched _ => Cegex.emptyset
   | Cegex.char char' =>
     if char' = char
-    then Cegex.epsilon
+    then Cegex.matched char
     else Cegex.emptyset
   | Cegex.or y z => Cegex.smartOr (derive y char) (derive z char)
   | Cegex.concat y z =>
@@ -38,16 +40,17 @@ partial def derive (x: Cegex) (char: Char): Cegex :=
   | Cegex.star y => Cegex.smartConcat (derive y char) x
   -- group is the new operator compared to Expr.
   -- We store the input tree in the expression.
-  | Cegex.group n chars y =>
-    Cegex.group n (char :: chars) (derive y char)
+  | Cegex.group n y =>
+    Cegex.group n (derive y char)
 
-def extract (x: Cegex): List (Nat × List Char) :=
+def extract (x: Cegex): List Char :=
   match x with
   -- should never be encountered, since emptyset is not nullable.
   | Cegex.emptyset => []
   | Cegex.epsilon => []
   -- should never be encountered, since char is not nullable.
   | Cegex.char _ => []
+  | Cegex.matched c => [c]
   | Cegex.or y z =>
     -- Under POSIX semantics, we prefer matching the left alternative.
     if y.nullable
@@ -58,12 +61,34 @@ def extract (x: Cegex): List (Nat × List Char) :=
     -- Groups under a star are ignored.
     -- Recursively extracting under the star causes empty captures to be reported, which we do not want under POSIX semantics.
   | Cegex.star _ => []
-  | Cegex.group id c y => (id, c) :: extract y
+    -- ignore group, this group will be extracted later by extractGroups.
+  | Cegex.group _ y => extract y
+
+def extractGroups (x: Cegex): List (Nat × List Char) :=
+  match x with
+  -- should never be encountered, since emptyset is not nullable.
+  | Cegex.emptyset => []
+  | Cegex.epsilon => []
+  -- should never be encountered, since char is not nullable.
+  | Cegex.char _ => []
+  | Cegex.matched _ => []
+  | Cegex.or y z =>
+    -- Under POSIX semantics, we prefer matching the left alternative.
+    if y.nullable
+    then extractGroups y
+    else extractGroups z
+  | Cegex.concat y z =>
+    extractGroups y ++ extractGroups z
+    -- Groups under a star are ignored.
+    -- Recursively extracting under the star causes empty captures to be reported, which we do not want under POSIX semantics.
+  | Cegex.star _ => []
+    -- extract the string
+  | Cegex.group id y => (id, extract y) :: extractGroups y
 
 def captures (x: Cegex) (chars: List Char): Option (List (Nat × List Char)) :=
   let dx := List.foldl derive x chars
   if dx.nullable
-  then Option.some (extract dx)
+  then Option.some (extractGroups dx)
   else Option.none
 
 def capture (name: Nat) (x: Cegex) (input: String): Option String :=
@@ -82,23 +107,23 @@ def capture (name: Nat) (x: Cegex) (input: String): Option String :=
 
 #guard capture 1 (Cegex.concat (Cegex.concat
     (Cegex.star (Cegex.char 'a'))
-    (Cegex.group 1 [] (Cegex.char 'b')))
+    (Cegex.group 1 (Cegex.char 'b')))
     (Cegex.star (Cegex.char 'a'))
   )
   "aaabaaa" =
   Option.some "b"
 
 #guard capture 1 (Cegex.concat (Cegex.concat
     (Cegex.star (Cegex.char 'a'))
-    (Cegex.group 1 [] (Cegex.star (Cegex.char 'b'))))
+    (Cegex.group 1 (Cegex.star (Cegex.char 'b'))))
     (Cegex.star (Cegex.char 'a'))
   )
   "aaabbbaaa" =
   Option.some "bbb"
 
 #guard capture 1 (Cegex.concat (Cegex.concat
     (Cegex.star (Cegex.char 'a'))
-    (Cegex.group 1 []
+    (Cegex.group 1
       (Cegex.or
         (Cegex.star (Cegex.char 'b'))
         (Cegex.star (Cegex.char 'c'))
@@ -108,3 +133,16 @@ def capture (name: Nat) (x: Cegex) (input: String): Option String :=
   )
   "aaacccaaa" =
   Option.some "ccc"
+
+#guard capture 1 (Cegex.concat (Cegex.concat
+    (Cegex.star (Cegex.char 'a'))
+    (Cegex.group 1
+      (Cegex.or
+        (Cegex.star (Cegex.char 'b'))
+        (Cegex.concat (Cegex.char 'b') (Cegex.star (Cegex.char 'c')))
+      )
+    ))
+    (Cegex.star (Cegex.char 'a'))
+  )
+  "aaabccaaa" =
+  Option.some "bcc"

Validator/Learning/Regex/RegexCapture.lean

@@ -39,7 +39,7 @@ partial def derive (x: Regex) (char: Char): Regex :=
   -- group is the new operator compared to Expr.
   -- We store the input tree in the expression.
   | Regex.group n chars y =>
-    Regex.group n (char :: chars) (derive y char)
+    Regex.group n (chars ++ [char]) (derive y char)
 
 def extract (x: Regex): List (Nat × List Char) :=
   match x with
@@ -108,3 +108,16 @@ def capture (name: Nat) (x: Regex) (input: String): Option String :=
   )
   "aaacccaaa" =
   Option.some "ccc"
+
+#guard capture 1 (Regex.concat (Regex.concat
+    (Regex.star (Regex.char 'a'))
+    (Regex.group 1 []
+      (Regex.or
+        (Regex.star (Regex.char 'b'))
+        (Regex.concat (Regex.char 'b') (Regex.star (Regex.char 'c')))
+      )
+    ))
+    (Regex.star (Regex.char 'a'))
+  )
+  "aaabccaaa" =
+  Option.some "bcc"