Add ParseOption to regex parser for case-insensitive mode

Author: yuuki14202028

regex/Regex/Regex/Basic.lean

@@ -81,15 +81,24 @@ def fromExpr (expr : Expr) : Regex :=
   { nfa := nfa, wf := Regex.NFA.compile_wf, optimizationInfo := optimizationInfo }
 
 /--
-Parses a regular expression string into a `Regex` structure.
-
+Parses a regular expression string into a `Regex` structure with options.
 * `s`: The regular expression string to parse
+* `options`: Parsing options
 * Returns: Either a compiled `Regex` or a parsing error
 -/
-def parse (s : String) : Except Regex.Syntax.Parser.Error Regex := do
-  let expr ← Regex.Syntax.Parser.parse s
+def parseAux (s : String) (options : Regex.Syntax.Parser.ParseOption) : Except Regex.Syntax.Parser.Error Regex := do
+  let expr ← Regex.Syntax.Parser.parseAux s options
   return Regex.fromExpr expr
 
+/--
+Parses a regular expression string into a `Regex` structure with default options.
+
+* `s`: The regular expression string to parse
+* Returns: Either a compiled `Regex` or a parsing error
+-/
+def parse (s : String) : Except Regex.Syntax.Parser.Error Regex :=
+  parseAux s {}
+
 /--
 Parses a regular expression string into a `Regex` structure, panicking on parse error.
 

regex/Regex/Syntax/Parser/Basic.lean

@@ -333,14 +333,19 @@ termination_by (pos, 100)
 
 end
 
+structure ParseOption where
+  caseInsensitive : Bool := false
+
 def parseAst (input : String) : Except Error Ast :=
   regex input.startPos
   |>.complete .expectedEof
   |>.toExcept
 
-def parse (input : String) : Except Error Expr :=
+def parseAux (input : String) (options : ParseOption) : Except Error Expr :=
   parseAst input
-  |>.map fun ast => Ast.toRegex (.group ast)
+  |>.map fun ast => Ast.toRegexAux (ToRegexState.mk 0 options.caseInsensitive) (.group ast) |>.2
+
+def parse (input : String) : Except Error Expr := parseAux input {}
 
 def parse! (input : String) : Expr :=
   match parse input with