add copy for Regex implementation for experimentation

Author: awalterschulze

Validator/Learning.lean

@@ -9,3 +9,6 @@ import Validator.Learning.Parser
 
 import Validator.Learning.Regex.Regex
 import Validator.Learning.Regex.RegexCapture
+
+import Validator.Learning.Cegex.Cegex
+import Validator.Learning.Cegex.CegexCapture

Validator/Learning/Cegex/Cegex.lean

@@ -0,0 +1,51 @@
+-- Cegex includes capturing groups
+inductive Cegex where
+  | emptyset
+  | epsilon
+  | 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)
+  deriving DecidableEq, Ord, Repr, Hashable
+
+def Cegex.nullable (x: Cegex): Bool :=
+  match x with
+  | Cegex.emptyset => false
+  | Cegex.epsilon => 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
+
+def Cegex.unescapable (x: Cegex): Bool :=
+  match x with
+  | Cegex.emptyset => true
+  | _ => false
+
+-- smartOr is a smart constructor for the or operator.
+def Cegex.smartOr (x y: Cegex): Cegex :=
+  match x with
+  | Cegex.emptyset => y
+  | _ =>
+    match y with
+    | Cegex.emptyset => x
+    | _ => Cegex.or x y
+
+-- smartConcat is a smart constructor for the concat operator.
+def Cegex.smartConcat (x y: Cegex): Cegex :=
+  match x with
+  | Cegex.emptyset => Cegex.emptyset
+  | _ =>
+    match y with
+    | Cegex.emptyset => Cegex.emptyset
+    | _ => Cegex.concat x y
+
+-- smartStar is a smart constructor for the star operator.
+def Cegex.smartStar (x: Cegex): Cegex :=
+  match x with
+  | Cegex.star _ => x
+  | _ => Cegex.star x

Validator/Learning/Cegex/CegexCapture.lean

@@ -0,0 +1,110 @@
+-- This algorithm is from Regular Expression Sub-Matching using Partial Derivatives - Martin Sulzmann and Kenny Zhuo Ming Lu
+
+-- Thank you Keegan Perry for simplifying and explaining this to me.
+import Validator.Learning.Cegex.Cegex
+
+namespace CegexCapture
+
+-- neutralize replaces all chars with emptyset.
+-- This way the expression will stay nullable and not change based on derivative input.
+-- This makes it possible to keep all the capture groups inside for later extraction.
+def neutralize (x: Cegex): Cegex :=
+  match x with
+  | Cegex.emptyset => Cegex.emptyset
+  | Cegex.epsilon => Cegex.epsilon
+  | 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)
+
+partial def derive (x: Cegex) (char: Char): Cegex :=
+  match x with
+  | Cegex.emptyset => Cegex.emptyset
+  | Cegex.epsilon => Cegex.emptyset
+  | Cegex.char char' =>
+    if char' = char
+    then Cegex.epsilon
+    else Cegex.emptyset
+  | Cegex.or y z => Cegex.smartOr (derive y char) (derive z char)
+  | Cegex.concat y z =>
+    if Cegex.nullable y
+    then Cegex.smartOr
+      (Cegex.smartConcat (derive y char) z)
+      -- A difference from the usual derive algorithm:
+      -- Instead of (derive z tree), we write:
+      (Cegex.smartConcat (neutralize y) (derive z char))
+    else Cegex.concat (derive y char) z
+  | 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)
+
+def extract (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.or y z =>
+    -- Under POSIX semantics, we prefer matching the left alternative.
+    if y.nullable
+    then extract y
+    else extract z
+  | Cegex.concat y z =>
+    extract y ++ extract 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 _ => []
+  | Cegex.group id c y => (id, c) :: extract 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)
+  else Option.none
+
+def capture (name: Nat) (x: Cegex) (input: String): Option String :=
+  match input with
+  | String.mk chars =>
+  match captures x chars with
+  | Option.none => Option.none
+  | Option.some cs =>
+  let strs := List.filterMap
+    (fun (name', str) =>
+      if name = name'
+      then Option.some (String.mk str)
+      else Option.none
+    ) cs
+  List.head? (List.reverse (List.mergeSort strs))
+
+#guard capture 1 (Cegex.concat (Cegex.concat
+    (Cegex.star (Cegex.char 'a'))
+    (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.star (Cegex.char 'a'))
+  )
+  "aaabbbaaa" =
+  Option.some "bbb"
+
+#guard capture 1 (Cegex.concat (Cegex.concat
+    (Cegex.star (Cegex.char 'a'))
+    (Cegex.group 1 []
+      (Cegex.or
+        (Cegex.star (Cegex.char 'b'))
+        (Cegex.star (Cegex.char 'c'))
+      )
+    ))
+    (Cegex.star (Cegex.char 'a'))
+  )
+  "aaacccaaa" =
+  Option.some "ccc"

Validator/Learning/Regex/RegexCapture.lean

@@ -1,18 +1,22 @@
 -- This algorithm is from Regular Expression Sub-Matching using Partial Derivatives - Martin Sulzmann and Kenny Zhuo Ming Lu
 
+-- Thank you Keegan Perry for simplifying and explaining this to me.
 import Validator.Learning.Regex.Regex
 
 namespace RegexCapture
 
-def charToEmptySet (x: Regex): Regex :=
+-- neutralize replaces all chars with emptyset.
+-- This way the expression will stay nullable and not change based on derivative input.
+-- This makes it possible to keep all the capture groups inside for later extraction.
+def neutralize (x: Regex): Regex :=
   match x with
   | Regex.emptyset => Regex.emptyset
   | Regex.epsilon => Regex.epsilon
   | Regex.char _ => Regex.emptyset
-  | Regex.or y z => Regex.smartOr (charToEmptySet y) (charToEmptySet z)
-  | Regex.concat y z => Regex.concat (charToEmptySet y) (charToEmptySet z)
-  | Regex.star y => Regex.star (charToEmptySet y)
-  | Regex.group id c y => Regex.group id c (charToEmptySet y)
+  | Regex.or y z => Regex.smartOr (neutralize y) (neutralize z)
+  | Regex.concat y z => Regex.concat (neutralize y) (neutralize z)
+  | Regex.star y => Regex.star (neutralize y)
+  | Regex.group id c y => Regex.group id c (neutralize y)
 
 partial def derive (x: Regex) (char: Char): Regex :=
   match x with
@@ -29,7 +33,7 @@ partial def derive (x: Regex) (char: Char): Regex :=
       (Regex.smartConcat (derive y char) z)
       -- A difference from the usual derive algorithm:
       -- Instead of (derive z tree), we write:
-      (Regex.smartConcat (charToEmptySet y) (derive z char))
+      (Regex.smartConcat (neutralize y) (derive z char))
     else Regex.concat (derive y char) z
   | Regex.star y => Regex.smartConcat (derive y char) x
   -- group is the new operator compared to Expr.