Parse

Parse the regular expression (parse)

structure Regex.Syntax.AstItems.Parser : Type

State of the parser

• capture_index : Nat

  The current capture index.

• capture_group_names : List (Nat × String)

  The names of capture groups.

• max_backreference : Nat

  The maximal single digit backreference.

@[implicit_reducible]

instance Regex.Syntax.AstItems.instInhabitedParser : Inhabited AstItems.Parser

Equations

• Regex.Syntax.AstItems.instInhabitedParser = { default := { capture_index := 0, capture_group_names := [], max_backreference := 0 } }

@[reducible, inline]

abbrev Regex.Syntax.AstItems.ParserM (α : Type) : Type

Equations

• Regex.Syntax.AstItems.ParserM = ReaderT Regex.Syntax.Flavor (StateT Regex.Syntax.AstItems.Parser (Except String))

def Regex.Syntax.AstItems.valuesOfLitSyntax (x : Lean.Syntax) : Option (Lean.SyntaxNodeKind × Lean.SourceInfo × String)

match syntax make by Lean.Syntax.mkLit

Equations

• Regex.Syntax.AstItems.valuesOfLitSyntax x = match x with | Lean.Syntax.node info k #[Lean.Syntax.atom info_1 s] => some (k, info_1, s) | x => none

def Regex.Syntax.AstItems.valueOfLitSyntax (x : Lean.Syntax) (kind : Lean.SyntaxNodeKind) : Option String

Equations

• Regex.Syntax.AstItems.valueOfLitSyntax x kind = match x with | Lean.Syntax.node info k #[Lean.Syntax.atom info_1 s] => if k = kind then some s else none | x => none

def Regex.Syntax.AstItems.extractNegated (arr : Array Lean.Syntax) : Bool × { arr' : Array Lean.Syntax // sizeOf arr' ≤ sizeOf arr }

Equations

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

def Regex.Syntax.AstItems.firstChar (s : String) : ParserM Char

Equations

• Regex.Syntax.AstItems.firstChar s = if s.length = 1 then pure (String.Pos.Raw.get s 0) else liftM (Except.error (toString "ill-formed literal syntax " ++ toString s))

def Regex.Syntax.AstItems.parseLiteral (p : String) (x : Lean.Syntax) : ParserM Ast

Equations

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

def Regex.Syntax.AstItems.parseHyphen (p : String) (x : Lean.Syntax) : ParserM Ast

Equations

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

def Regex.Syntax.AstItems.nameToClassSetItems : List (String × ClassAsciiKind)

Equations

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

def Regex.Syntax.AstItems.parsePosixCharacterClass (p : String) (x : Lean.Syntax) : ParserM ClassSetItem

Equations

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

def Regex.Syntax.AstItems.parseDot (p : String) (x : Lean.Syntax) : ParserM Ast

Equations

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

def Regex.Syntax.AstItems.getPerlClass (c : Char) : ParserM (Bool × ClassPerlKind)

Equations

• Regex.Syntax.AstItems.getPerlClass 'd' = pure (false, Regex.Syntax.AstItems.ClassPerlKind.Digit)
• Regex.Syntax.AstItems.getPerlClass 'D' = pure (true, Regex.Syntax.AstItems.ClassPerlKind.Digit)
• Regex.Syntax.AstItems.getPerlClass 'h' = pure (false, Regex.Syntax.AstItems.ClassPerlKind.HorizontalSpace)
• Regex.Syntax.AstItems.getPerlClass 'H' = pure (true, Regex.Syntax.AstItems.ClassPerlKind.HorizontalSpace)
• Regex.Syntax.AstItems.getPerlClass 'n' = pure (false, Regex.Syntax.AstItems.ClassPerlKind.Newline)
• Regex.Syntax.AstItems.getPerlClass 'N' = pure (true, Regex.Syntax.AstItems.ClassPerlKind.Newline)
• Regex.Syntax.AstItems.getPerlClass 's' = pure (false, Regex.Syntax.AstItems.ClassPerlKind.Space)
• Regex.Syntax.AstItems.getPerlClass 'S' = pure (true, Regex.Syntax.AstItems.ClassPerlKind.Space)
• Regex.Syntax.AstItems.getPerlClass 'v' = pure (false, Regex.Syntax.AstItems.ClassPerlKind.VerticalSpace)
• Regex.Syntax.AstItems.getPerlClass 'V' = pure (true, Regex.Syntax.AstItems.ClassPerlKind.VerticalSpace)
• Regex.Syntax.AstItems.getPerlClass 'w' = pure (false, Regex.Syntax.AstItems.ClassPerlKind.Word)
• Regex.Syntax.AstItems.getPerlClass 'W' = pure (true, Regex.Syntax.AstItems.ClassPerlKind.Word)
• Regex.Syntax.AstItems.getPerlClass c = liftM (Except.error (toString "expected valid Perl class but got " ++ toString c))

def Regex.Syntax.AstItems.parseGenericCharacterType (p : String) (x : Lean.Syntax) : ParserM Ast

Equations

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

def Regex.Syntax.AstItems.parseUnicodeCharacterProperty (p : String) (x : Lean.Syntax) : ParserM Ast

Equations

• One or more equations did not get rendered due to their size.
• Regex.Syntax.AstItems.parseUnicodeCharacterProperty p x = liftM (Except.error (toString "no UnicodeCharacterProperty values in " ++ toString x))

def Regex.Syntax.AstItems.parseBackReference (p : String) (x : Lean.Syntax) : ParserM Ast

Equations

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

def Regex.Syntax.AstItems.parseBackReferenceOrLiteral (p : String) (x : Lean.Syntax) : ParserM Ast

Equations

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

def Regex.Syntax.AstItems.parseAssertion (p : String) (x : Lean.Syntax) : ParserM Ast

Equations

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

def Regex.Syntax.AstItems.toFlags (chars : List Char) : ParserM (Array FlagsItem)

Equations

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

def Regex.Syntax.AstItems.parseGroupKind (p : String) (x : Lean.Syntax) : ParserM GroupKind

Equations

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

def Regex.Syntax.AstItems.toConcat (asts : Array Ast) : Ast

Equations

• Regex.Syntax.AstItems.toConcat asts = match asts with | #[ast] => ast | x => Regex.Syntax.AstItems.Ast.Concat (Regex.Syntax.AstItems.Concat.mk "".toRawSubstring asts)

def Regex.Syntax.AstItems.toRepetitionKind (p l r : String) : ParserM RepetitionKind

Equations

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

def Regex.Syntax.AstItems.toRepetition (p : String) (f t : String.Pos.Raw) (l r m : String) (ast : Ast) : ParserM Ast

Equations

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

def Regex.Syntax.AstItems.toClassSetItem (ast : Ast) : ParserM ClassSetItem

Equations

• Regex.Syntax.AstItems.toClassSetItem (Regex.Syntax.AstItems.Ast.Literal lit) = pure (Regex.Syntax.AstItems.ClassSetItem.Literal lit)
• Regex.Syntax.AstItems.toClassSetItem (Regex.Syntax.AstItems.Ast.ClassPerl cls) = pure (Regex.Syntax.AstItems.ClassSetItem.Perl cls)
• Regex.Syntax.AstItems.toClassSetItem (Regex.Syntax.AstItems.Ast.ClassUnicode cls) = pure (Regex.Syntax.AstItems.ClassSetItem.Unicode cls)
• Regex.Syntax.AstItems.toClassSetItem (Regex.Syntax.AstItems.Ast.ClassBracketed cls) = pure (Regex.Syntax.AstItems.ClassSetItem.Bracketed cls)
• Regex.Syntax.AstItems.toClassSetItem ast = liftM (Except.error (toString "unexpected ast for class set item " ++ toString ast))

def Regex.Syntax.AstItems.rangeToClassSetItem (p : String) (a b : Lean.Syntax) : ParserM ClassSetItem

Equations

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

def Regex.Syntax.AstItems.set_width (pattern : String) (g : Group) : ParserM Group

set fixed width for look behind

Equations

• One or more equations did not get rendered due to their size.
• Regex.Syntax.AstItems.set_width pattern g = pure g

def Regex.Syntax.AstItems.unfoldUnion (union : ClassSetUnion) : ClassSetItem ⊕ ClassSetBinaryOp

Equations

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

def Regex.Syntax.AstItems.toNode? (t : Lean.Syntax) : Option { x : Lean.SourceInfo × Lean.SyntaxNodeKind × Array Lean.Syntax // sizeOf x.snd.snd < sizeOf t }

Equations

• Regex.Syntax.AstItems.toNode? (Lean.Syntax.node si kind args) = some ⟨(si, kind, args), ⋯⟩
• Regex.Syntax.AstItems.toNode? t = none

def Regex.Syntax.AstItems.parseSimpleClassSetItem (p : String) (x : Lean.Syntax) (kind : Lean.SyntaxNodeKind) (arr : Array Lean.Syntax) : ParserM (Option ClassSetItem)

Equations

• One or more equations did not get rendered due to their size.
• Regex.Syntax.AstItems.parseSimpleClassSetItem p x `whitespace arr = pure (some (Regex.Syntax.AstItems.ClassSetItem.Empty "".toRawSubstring))
• Regex.Syntax.AstItems.parseSimpleClassSetItem p x `literal arr = do let __do_lift ← Regex.Syntax.AstItems.parseLiteral p x >>= Regex.Syntax.AstItems.toClassSetItem pure (some __do_lift)
• Regex.Syntax.AstItems.parseSimpleClassSetItem p x `hyphen arr = do let __do_lift ← Regex.Syntax.AstItems.parseHyphen p x >>= Regex.Syntax.AstItems.toClassSetItem pure (some __do_lift)
• Regex.Syntax.AstItems.parseSimpleClassSetItem p x `range arr = do let __do_lift ← Regex.Syntax.AstItems.rangeToClassSetItem p arr[0]! arr[1]! pure (some __do_lift)
• Regex.Syntax.AstItems.parseSimpleClassSetItem p x `posixCharacterClass arr = do let a ← Regex.Syntax.AstItems.parsePosixCharacterClass p x pure (some a)
• Regex.Syntax.AstItems.parseSimpleClassSetItem p x `endQuote arr = throw (Regex.Syntax.AstItems.toError p Regex.Syntax.AstItems.ErrorKind.EndQuoteWithoutOpenQuote)
• Regex.Syntax.AstItems.parseSimpleClassSetItem p x kind arr = pure none

def Regex.Syntax.AstItems.parseSimpleVal (p : String) (x : Lean.Syntax) : ParserM (Option Ast)

Equations

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

@[irreducible]

def Regex.Syntax.AstItems.parseClassSetItem (p : String) (x : Lean.Syntax) : ParserM ClassSetItem

Equations

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

@[irreducible]

def Regex.Syntax.AstItems.parseVal (p : String) (x : Lean.Syntax) : ParserM Ast

Equations

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

def Regex.Syntax.AstItems.folder (p : String) (acc : Array Ast) (x : Lean.Syntax) (parse : String → Lean.Syntax → ParserM Ast) : ParserM (Array Ast)

Equations

• Regex.Syntax.AstItems.folder p acc x parse = do let ast ← parse p x pure (acc ++ #[ast])

@[irreducible]

def Regex.Syntax.AstItems.fold (p : String) (arr : Array Lean.Syntax) : ParserM (Array Ast)

Equations

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

@[irreducible]

def Regex.Syntax.AstItems.parseGroup (p : String) (f t : String.Pos.Raw) (arr : Array Lean.Syntax) : ParserM Ast

Equations

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

@[irreducible]

def Regex.Syntax.AstItems.parseAlternatives (p : String) (arr : Array Lean.Syntax) : ParserM Ast

Equations

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

@[irreducible]

def Regex.Syntax.AstItems.parseRepetition (p : String) (f t : String.Pos.Raw) (arr : Array Lean.Syntax) : ParserM Ast

Equations

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

@[irreducible]

def Regex.Syntax.AstItems.innerParseCharacterClassSetOp (p op : String) (left right : Array Lean.Syntax) : ParserM Ast

Equations

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

@[irreducible]

def Regex.Syntax.AstItems.parseCharacterClassSetOp (p : String) (arr : Array Lean.Syntax) : ParserM Ast

Equations

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

@[irreducible]

def Regex.Syntax.AstItems.parseCharacterClass (p : String) (arr : Array Lean.Syntax) : ParserM Ast

Equations

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

@[irreducible]

def Regex.Syntax.AstItems.parseSequence (p : String) (arr : Array Lean.Syntax) : ParserM Ast

Equations

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

def Regex.Syntax.AstItems.parseSequence' (p : String) (x : Lean.Syntax) : ParserM Ast

Equations

• Regex.Syntax.AstItems.parseSequence' p (Lean.Syntax.node info `sequence arr) = Regex.Syntax.AstItems.parseSequence p arr
• Regex.Syntax.AstItems.parseSequence' p x = liftM (Except.error (toString "ill-formed sequence syntax " ++ toString x))

def Regex.Syntax.AstItems.parse (p : String) (flavor : Flavor) (extended : Grammar.ExtendedKind := Grammar.ExtendedKind.None) : Except String Ast

Parse the regular expression and return an abstract syntax tree.

Equations

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