better comments

Author: awalterschulze

Validator/Derive/Enter.lean

@@ -7,7 +7,7 @@ def enter (x: Expr) (res: List IfExpr := []): List IfExpr :=
   match x with
   | Expr.emptyset => res
   | Expr.epsilon => res
-  | Expr.tree p y => (IfExpr.mk p y Expr.emptyset) :: res
+  | Expr.tree pred childrenExpr => (IfExpr.mk pred childrenExpr Expr.emptyset) :: res
   | Expr.or y z => enter y (enter z res)
   | Expr.concat y z =>
     if Expr.nullable y

Validator/Learning/Cegex/Cegex.lean

@@ -2,6 +2,7 @@
 inductive Cegex where
   | emptyset
   | epsilon
+  -- NEW: matched operator
   | matched (c: Char)
   | char (c: Char)
   | or (y z: Cegex)

Validator/Learning/Parser.lean

@@ -27,7 +27,7 @@ def deriveLeave [ValidateM m] (xs: List Expr) (cs: List Expr): m (List Expr) :=
   Leave.DeriveLeave.deriveLeave xs (List.map Expr.nullable cs)
 
 def deriveValue [ValidateM m] (xs: List Expr): m (List Expr) := do
-  deriveLeave xs (<- deriveEnter xs)
+  deriveEnter xs >>= deriveLeave xs
 
 -- TODO: Is it possible to have a Parser type that can be proved to be of the correct shape, and have not expection throwing
 -- for example: can you prove that your Parser will never return an Hint.leave after returning a Hint.field.

Validator/Learning/Regex/RegexCapture.lean

@@ -12,6 +12,7 @@ def neutralize (x: Regex): Regex :=
   match x with
   | Regex.emptyset => Regex.emptyset
   | Regex.epsilon => Regex.epsilon
+  -- only char changes to emptyset
   | Regex.char _ => Regex.emptyset
   | Regex.or y z => Regex.smartOr (neutralize y) (neutralize z)
   | Regex.concat y z => Regex.concat (neutralize y) (neutralize z)

Validator/Learning/Tegex/Tegex.lean

@@ -5,19 +5,21 @@ import Validator.Parser.ParseTree
 inductive Tegex where
   | emptyset
   | epsilon
+  -- Cegex.matched is extended to trees
   | matched (tok: Token) (childExpr: Tegex)
   | tree (tok: Token) (childExpr: Tegex)
   | or (y z: Tegex)
   | concat (y z: Tegex)
   | star (y: Tegex)
-  -- group is the only new operator compared to a Tegex without capturing groups.
+  -- group is a copy of Cegex.group without the captured string.
   | group (id: Nat) (x: Tegex)
   deriving DecidableEq, Ord, Repr, Hashable
 
 def Tegex.nullable (x: Tegex): Bool :=
   match x with
   | Tegex.emptyset => false
   | Tegex.epsilon => true
+  -- matched is technically the same as epsilon, except that it stores the matched token and childExpr.
   | Tegex.matched _ _ => true
   | Tegex.tree _ _ => false
   | Tegex.or y z => nullable y || nullable z

Validator/Learning/Tegex/TegexCapture.lean

@@ -8,9 +8,9 @@ import Validator.Learning.Tegex.Tegex
 
 namespace TegexCapture
 
--- 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.
+-- neutralize replaces all tree operators with emptyset.
+-- It is used when deriving concat.
+-- This way we do not lose capture information on nullable expressions.
 def neutralize (x: Tegex): Tegex :=
   match x with
   | Tegex.emptyset => Tegex.emptyset
@@ -26,6 +26,7 @@ partial def derive (x: Tegex) (tree: ParseTree): Tegex :=
   match x with
   | Tegex.emptyset => Tegex.emptyset
   | Tegex.epsilon => Tegex.emptyset
+  -- remember matched is just epsilon, so has the same derivative.
   | Tegex.matched _ _ => Tegex.emptyset
   | Tegex.tree tok' childExpr =>
     match tree with
@@ -43,12 +44,11 @@ partial def derive (x: Tegex) (tree: ParseTree): Tegex :=
     then Tegex.smartOr
       (Tegex.smartConcat (derive y tree) z)
       -- A difference from the usual derive algorithm:
-      -- Instead of (derive z tree), we write:
+      -- To preserve the capture information in the nullable expression y,
+      -- instead of (derive z tree), we write:
       (Tegex.smartConcat (neutralize y) (derive z tree))
     else Tegex.concat (derive y tree) z
   | Tegex.star y => Tegex.smartConcat (derive y tree) x
-  -- group is the new operator compared to Expr.
-  -- We store the input tree in the expression.
   | Tegex.group n y =>
     Tegex.group n (derive y tree)
 
@@ -57,7 +57,7 @@ def extract (x: Tegex): List ParseTree :=
   -- should never be encountered, since emptyset is not nullable.
   | Tegex.emptyset => []
   | Tegex.epsilon => []
-  -- should never be encountered, since char is not nullable.
+  -- should never be encountered, since tree is not nullable.
   | Tegex.tree _ _ => []
   | Tegex.matched tok childExpr => [ParseTree.mk tok (extract childExpr)]
   | Tegex.or y z =>
@@ -70,7 +70,7 @@ def extract (x: Tegex): List ParseTree :=
     -- 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.
   | Tegex.star _ => []
-    -- ignore group, this group will be extracted later by extractGroups.
+    -- Ignore group, this group will be extracted later by extractGroups.
   | Tegex.group _ y => extract y
 
 def extractGroups (x: Tegex): List (Nat × List ParseTree) :=
@@ -80,6 +80,7 @@ def extractGroups (x: Tegex): List (Nat × List ParseTree) :=
   | Tegex.epsilon => []
   -- should never be encountered, since tree is not nullable.
   | Tegex.tree _ _ => []
+  -- There may be groups in the childExpr that needs to be extracted.
   | Tegex.matched _ childExpr => extractGroups childExpr
   | Tegex.or y z =>
     -- Under POSIX semantics, we prefer matching the left alternative.
@@ -91,7 +92,7 @@ def extractGroups (x: Tegex): List (Nat × List ParseTree) :=
     -- 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.
   | Tegex.star _ => []
-    -- extract the string
+    -- extract the forest for the single group id
   | Tegex.group id y => (id, extract y) :: extractGroups y
 
 def captures (x: Tegex) (forest: List ParseTree): Option (List (Nat × List ParseTree)) :=