inductive Strata.Python.ParseError : Type

• patternError (message pattern : String) (pos : String.Pos.Raw) : ParseError

  patternError is raised when Python's re.patternError exception is raised. Reference: Python's re exceptions:

  "Exception raised when a string passed to one of the functions here is not a valid regular expression (for example, it might contain unmatched parentheses) or when some other error occurs during compilation or matching. It is never an error if a string contains no match for a pattern."

• unimplemented (message pattern : String) (pos : String.Pos.Raw) : ParseError

  unimplemented is raised whenever we don't support some regex operations (e.g., lookahead assertions).

def Strata.Python.instReprParseError.repr : ParseError → Nat → Std.Format

Equations

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

instance Strata.Python.instReprParseError : Repr ParseError

Equations

• Strata.Python.instReprParseError = { reprPrec := Strata.Python.instReprParseError.repr }

def Strata.Python.ParseError.toString : ParseError → String

Equations

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

instance Strata.Python.instToStringParseError : ToString ParseError

Equations

• Strata.Python.instToStringParseError = { toString := Strata.Python.ParseError.toString }

inductive Strata.Python.RegexAST : Type

Regular Expression Nodes

• char : Char → RegexAST

  Single literal character: a

• range : Char → Char → RegexAST

  Character range: [a-z]

• union : RegexAST → RegexAST → RegexAST

  Alternation: a|b

• concat : RegexAST → RegexAST → RegexAST

  Concatenation: ab

• anychar : RegexAST

  Any character: .

• star : RegexAST → RegexAST

  Zero or more: a*

• plus : RegexAST → RegexAST

  One or more: a+

• optional : RegexAST → RegexAST

  Zero or one: a?

• loop : RegexAST → Nat → Nat → RegexAST

  Bounded repetition: a{n,m}

• anchor_start : RegexAST

  Start of string: ^

• anchor_end : RegexAST

  End of string: $

• group : RegexAST → RegexAST

  Grouping: (abc)

• empty : RegexAST

  Empty string: () or ""

• complement : RegexAST → RegexAST

  Complement: [^a-z]

def Strata.Python.instInhabitedRegexAST.default : RegexAST

Equations

• Strata.Python.instInhabitedRegexAST.default = Strata.Python.RegexAST.char default

instance Strata.Python.instInhabitedRegexAST : Inhabited RegexAST

Equations

• Strata.Python.instInhabitedRegexAST = { default := Strata.Python.instInhabitedRegexAST.default }

def Strata.Python.instReprRegexAST.repr : RegexAST → Nat → Std.Format

Equations

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

instance Strata.Python.instReprRegexAST : Repr RegexAST

Equations

• Strata.Python.instReprRegexAST = { reprPrec := Strata.Python.instReprRegexAST.repr }

def Strata.Python.parseCharClass (s : String) (pos : String.Pos.Raw) : Except ParseError (RegexAST × String.Pos.Raw)

Parse character class like [a-z], [0-9], etc. into union of ranges and chars. Note that this parses | as a character.

Equations

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

def Strata.Python.parseBounds (s : String) (pos : String.Pos.Raw) : Except ParseError (Nat × Nat × String.Pos.Raw)

Parse numeric repeats like {10} or {1,10} into min and max bounds.

Equations

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

partial def Strata.Python.parseAtom (s : String) (pos : String.Pos.Raw) : Except ParseError (RegexAST × String.Pos.Raw)

Parse atom: single element (char, class, anchor, group) with optional quantifier. Stops at the first |.

partial def Strata.Python.parseExplicitGroup (s : String) (pos : String.Pos.Raw) : Except ParseError (RegexAST × String.Pos.Raw)

Parse explicit group with parentheses.

partial def Strata.Python.parseGroup (s : String) (pos : String.Pos.Raw) (endChar : Option Char) : Except ParseError (RegexAST × String.Pos.Raw)

Parse group: handles alternation and concatenation at current scope.

def Strata.Python.parseTop (s : String) : Except ParseError RegexAST

Parse entire regex string (implicit top-level group).

Equations

• Strata.Python.parseTop s = Except.map (fun (x : Strata.Python.RegexAST × String.Pos.Raw) => match x with | (r, snd) => r) (Strata.Python.parseGroup s 0 none)