def Regex.Syntax.Parser.anyCharOrError : Combinators.Parser.LT Error Char

Equations

• Regex.Syntax.Parser.anyCharOrError = Regex.Syntax.Parser.Combinators.anyCharOrElse Regex.Syntax.Parser.Error.unexpectedEof

def Regex.Syntax.Parser.charOrError (c : Char) : Combinators.Parser.LT Error Char

Equations

• Regex.Syntax.Parser.charOrError c = Regex.Syntax.Parser.Combinators.charOrElse c Regex.Syntax.Parser.Error.unexpectedEof Regex.Syntax.Parser.Error.unexpectedChar

def Regex.Syntax.Parser.digit : Combinators.Parser.LT Error Nat

Equations

• One or more equations did not get rendered due to their size.

def Regex.Syntax.Parser.number : Combinators.Parser.LT Error Nat

Equations

• Regex.Syntax.Parser.number = Regex.Syntax.Parser.Combinators.foldl1 (fun (n d : Nat) => 10 * n + d) Regex.Syntax.Parser.digit

def Regex.Syntax.Parser.hexDigit : Combinators.Parser.LT Error Nat

Equations

• One or more equations did not get rendered due to their size.

def Regex.Syntax.Parser.hexNumberN (n : Nat) [NeZero n] : Combinators.Parser.LT Error Nat

Equations

• Regex.Syntax.Parser.hexNumberN n = Regex.Syntax.Parser.Combinators.foldlPos 0 (fun (n d : Nat) => 16 * n + d) Regex.Syntax.Parser.hexDigit n

def Regex.Syntax.Parser.specialCharacters : String

Equations

• Regex.Syntax.Parser.specialCharacters = "[](){*+?|^$.\\"

def Regex.Syntax.Parser.escapedChar : Combinators.Parser.LT Error (Char ⊕ Data.PerlClass)

Equations

• One or more equations did not get rendered due to their size.

def Regex.Syntax.Parser.escapedChar.simple : Combinators.Parser.LT Error Char

Equations

• One or more equations did not get rendered due to their size.

def Regex.Syntax.Parser.escapedChar.hex2 : Combinators.Parser.LT Error Char

Equations

• Regex.Syntax.Parser.escapedChar.hex2 = Regex.Syntax.Parser.charOrError 'x' *> Regex.Syntax.Parser.Combinators.Parser.commit (Char.ofNat <$> Regex.Syntax.Parser.hexNumberN 2)

def Regex.Syntax.Parser.escapedChar.hex4 : Combinators.Parser.LT Error Char

Equations

• Regex.Syntax.Parser.escapedChar.hex4 = Regex.Syntax.Parser.charOrError 'u' *> Regex.Syntax.Parser.Combinators.Parser.commit (Char.ofNat <$> Regex.Syntax.Parser.hexNumberN 4)

def Regex.Syntax.Parser.escapedChar.perlClass : Combinators.Parser.LT Error Data.PerlClass

Equations

• One or more equations did not get rendered due to their size.

def Regex.Syntax.Parser.escapedCharToAst (c : Char ⊕ Data.PerlClass) : Ast

Equations

• Regex.Syntax.Parser.escapedCharToAst (Sum.inl c_2) = Regex.Syntax.Parser.Ast.char c_2
• Regex.Syntax.Parser.escapedCharToAst (Sum.inr cls) = Regex.Syntax.Parser.Ast.perl cls

def Regex.Syntax.Parser.plainChar : Combinators.Parser.LT Error Char

Equations

• One or more equations did not get rendered due to their size.

def Regex.Syntax.Parser.anchor : Combinators.Parser.LT Error Ast

Equations

• One or more equations did not get rendered due to their size.

def Regex.Syntax.Parser.dot : Combinators.Parser.LT Error Ast

Equations

• Regex.Syntax.Parser.dot = Regex.Syntax.Parser.Combinators.Parser.mapConst Regex.Syntax.Parser.Ast.dot (Regex.Syntax.Parser.charOrError '.')

def Regex.Syntax.Parser.charInClass : Combinators.Parser.LT Error (Char ⊕ Data.PerlClass)

Equations

• One or more equations did not get rendered due to their size.

def Regex.Syntax.Parser.range : Combinators.Parser.LT Error Data.Class

Equations

• One or more equations did not get rendered due to their size.

def Regex.Syntax.Parser.range.expectsChar (c : Char ⊕ Data.PerlClass) : Except Error Char

Equations

• Regex.Syntax.Parser.range.expectsChar (Sum.inl c_2) = Except.ok c_2
• Regex.Syntax.Parser.range.expectsChar (Sum.inr cls) = Except.error (Regex.Syntax.Parser.Error.unexpectedPerlClassInRange cls)

def Regex.Syntax.Parser.singleClass : Combinators.Parser.LT Error Data.Class

Equations

• Regex.Syntax.Parser.singleClass = (Regex.Syntax.Parser.range <|> Regex.Syntax.Parser.singleClass.charToClass <$> Regex.Syntax.Parser.charInClass)

def Regex.Syntax.Parser.singleClass.charToClass (c : Char ⊕ Data.PerlClass) : Data.Class

Equations

• Regex.Syntax.Parser.singleClass.charToClass (Sum.inl c_2) = Regex.Data.Class.single c_2
• Regex.Syntax.Parser.singleClass.charToClass (Sum.inr cls) = Regex.Data.Class.perl cls

def Regex.Syntax.Parser.classes : Combinators.Parser.LT Error Ast

Equations

• One or more equations did not get rendered due to their size.

def Regex.Syntax.Parser.repetitionOp : Combinators.Parser.LT Error (Nat × Option Nat)

Equations

• One or more equations did not get rendered due to their size.

def Regex.Syntax.Parser.repeatConcat (ast : Ast) (n : Nat) : Ast

Equations

• Regex.Syntax.Parser.repeatConcat ast n = Regex.Syntax.Parser.repeatConcat.go ast ast (n - 1)

def Regex.Syntax.Parser.repeatConcat.go (ast accum : Ast) : Nat → Ast

Equations

• Regex.Syntax.Parser.repeatConcat.go ast accum 0 = accum
• Regex.Syntax.Parser.repeatConcat.go ast accum n.succ = Regex.Syntax.Parser.repeatConcat.go ast (accum.concat ast) n

def Regex.Syntax.Parser.applyRepetition (min : Nat) (max : Option Nat) (ast : Ast) : Ast

Equations

• One or more equations did not get rendered due to their size.
• Regex.Syntax.Parser.applyRepetition 0 (some 1) ast = ast.alternate Regex.Syntax.Parser.Ast.epsilon
• Regex.Syntax.Parser.applyRepetition 0 none ast = ast.star
• Regex.Syntax.Parser.applyRepetition 1 none ast = ast.concat ast.star
• Regex.Syntax.Parser.applyRepetition min none ast = (Regex.Syntax.Parser.repeatConcat ast min).concat ast.star

def Regex.Syntax.Parser.nonCapturing : Combinators.Parser.LT Error Unit

Equations

• Regex.Syntax.Parser.nonCapturing = Regex.Syntax.Parser.Combinators.Parser.mapConst () (Regex.Syntax.Parser.charOrError '?' *> Regex.Syntax.Parser.charOrError ':')

@[irreducible]

def Regex.Syntax.Parser.group (it : String.Iterator) : Combinators.Result.LT it Error Ast

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Regex.Syntax.Parser.primary (it : String.Iterator) : Combinators.Result.LT it Error Ast

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Regex.Syntax.Parser.repetition1 (ast : Ast) (it : String.Iterator) : Combinators.Result.LE it Error Ast

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Regex.Syntax.Parser.repetition (it : String.Iterator) : Combinators.Result.LT it Error Ast

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Regex.Syntax.Parser.concat1 (ast : Ast) (it : String.Iterator) : Combinators.Result.LE it Error Ast

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Regex.Syntax.Parser.concat (it : String.Iterator) : Combinators.Result.LE it Error Ast

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Regex.Syntax.Parser.alternate1 (ast : Ast) (it : String.Iterator) : Combinators.Result.LE it Error Ast

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Regex.Syntax.Parser.alternate (it : String.Iterator) : Combinators.Result.LE it Error Ast

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Regex.Syntax.Parser.regex (it : String.Iterator) : Combinators.Result.LE it Error Ast

Equations

• Regex.Syntax.Parser.regex it = Regex.Syntax.Parser.Combinators.Result.weaken (Regex.Syntax.Parser.alternate it)

def Regex.Syntax.Parser.parseAst (input : String) : Except Error Ast

Equations

• Regex.Syntax.Parser.parseAst input = (Regex.Syntax.Parser.Combinators.Result.complete Regex.Syntax.Parser.Error.expectedEof (Regex.Syntax.Parser.regex input.mkIterator)).toExcept

def Regex.Syntax.Parser.parse (input : String) : Except Error Data.Expr

Equations

• Regex.Syntax.Parser.parse input = Except.map (fun (ast : Regex.Syntax.Parser.Ast) => ast.group.toRegex) (Regex.Syntax.Parser.parseAst input)

def Regex.Syntax.Parser.parse! (input : String) : Data.Expr

Equations

• One or more equations did not get rendered due to their size.