Abstract syntax tree for a single regular expression.

The abstract syntax tree Syntax.AstItems.Ast.

inductive Syntax.AstItems.ErrorKind : Type

The type of an error that occurred while building an AST.

• BackRefenceInvalid : ErrorKind

  Backrefence invalid.

• CaptureLimitExceeded : ErrorKind

  The capturing group limit was exceeded.

• ClassEscapeInvalid : ErrorKind

  An invalid escape sequence was found in a character class set.

• ClassRangeInvalid : ErrorKind

  An invalid character class range was found.

• ClassRangeLiteral : ErrorKind

  An invalid range boundary was found in a character class.

• ClassUnclosed : ErrorKind

  An opening [ was found with no corresponding closing ].

• DecimalInvalid : ErrorKind

  An invalid decimal number was given where one was expected.

• EndQuoteWithoutOpenQuote : ErrorKind

  End quote without a corresponding open quote.

• EscapeHexEmpty : ErrorKind

  A bracketed hex literal was empty.

• EscapeHexInvalid : ErrorKind

  A bracketed hex literal did not correspond to a Unicode scalar value.

• EscapeHexInvalidDigit : ErrorKind

  An invalid hexadecimal digit was found.

• EscapeUnexpectedEof : ErrorKind

  EOF was found before an escape sequence was completed.

• EscapeUnrecognized : ErrorKind

  An unrecognized escape sequence.

• FixedWidtExcpected : ErrorKind

  Fixed width in look behind

• FlagDanglingNegation : ErrorKind

  A dangling negation was used when setting flags, e.g., i-.

• FlagDuplicate : ErrorKind

  A flag was used twice, e.g., i-i.

• FlagRepeatedNegation : ErrorKind

  The negation operator was used twice, e.g., -i-s.

• FlagUnexpectedEof : ErrorKind

  Expected a flag but got EOF, e.g., (?.

• FlagUnrecognized : ErrorKind

  Unrecognized flag, e.g., a.

• GroupNameDuplicate : ErrorKind

  A duplicate capture name was found.

• GroupNameEmpty : ErrorKind

  A capture group name is empty, e.g., (?P<>abc).

• GroupNameInvalid : ErrorKind

  An invalid character was seen for a capture group name.

• GroupNameNotFound : ErrorKind

  A capture group name is not found of a backreference.

• GroupNameUnexpectedEof : ErrorKind

  A closing > could not be found for a capture group name.

• GroupUnclosed : ErrorKind

  An unclosed group, e.g., (ab.

• GroupUnopened : ErrorKind

  An unopened group, e.g., ab).

• NestLimitExceeded : ErrorKind

  The nest limit was exceeded.

• RepetitionCountInvalid : ErrorKind

  The range provided in a counted repetition operator is invalid.

• RepetitionCountDecimalEmpty : ErrorKind

  An opening { was not followed by a valid decimal value.

• RepetitionCountUnclosed : ErrorKind

  An opening { was found with no corresponding closing }.

• RepetitionMissing : ErrorKind

  A repetition operator was applied to a missing sub-expression.

• RepetitionUngreedyAndPossessive : ErrorKind

  A repetition operator was ungreedy and possessive.

• SpecialWordBoundaryUnclosed : ErrorKind

  The special word boundary syntax, \b{something}, was used, but either EOF without } was seen, or an invalid character in the braces was seen.

• SpecialWordBoundaryUnrecognized : ErrorKind

  The special word boundary syntax, \b{something}, was used, but something was not recognized as a valid word boundary kind.

• SpecialWordOrRepetitionUnexpectedEof : ErrorKind

  The syntax \b{ was observed, but afterwards the end of the pattern was observed without being able to tell whether it was meant to be a bounded repetition on the \b or the beginning of a special word boundary assertion.

• UnicodeClassInvalid : ErrorKind

  The Unicode class is not valid.

• UnsupportedBackreference : ErrorKind

  When octal support is disabled, this error is produced when an octal escape is used.

• UnsupportedLookAround : ErrorKind

  When syntax similar to PCRE's look-around is used, this error is returned.

• UnkownAsciiClass : ErrorKind

  ClassAsci not found.

• EscapeOctalInvalid : ErrorKind

  A octal literal did not correspond to a Unicode scalar value.

• FeatureNotImplementedSubroutines : ErrorKind

  Feature not implemented.

• FeatureNotImplementedFlagShorthand : ErrorKind

  Feature not implemented.

• FeatureNotImplementedAtomicGroup : ErrorKind

  Feature not implemented.

• FeatureNotImplementedConditionalExpression : ErrorKind

  Feature not implemented.

• FeatureNotImplementedBranchResetGroup : ErrorKind

  Feature not implemented.

• FeatureNotImplementedControlVerbs : ErrorKind

  Feature not implemented.

• FeatureNotImplementedFlagExtended : ErrorKind

  Feature not implemented.

def Syntax.AstItems.ErrorKind.toString : ErrorKind → String

instance Syntax.AstItems.instToStringErrorKind : ToString ErrorKind

Equations

• Syntax.AstItems.instToStringErrorKind = { toString := Syntax.AstItems.ErrorKind.toString }

def Syntax.AstItems.toError (s : String) (kind : ErrorKind) (msg : String := "") : String

Equations

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

def Syntax.AstItems.toErrorAt (s : String) (i : Nat) (kind : ErrorKind) (msg : String := "") : String

Equations

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

inductive Syntax.AstItems.HexLiteralKind : Type

The type of a Unicode hex literal.

• x : HexLiteralKind

  A \x prefix. When used without brackets, this form is limited to one digit (Pcre flavor).

• X : HexLiteralKind

  A \x prefix. When used without brackets, this form is limited to two digits.

• UnicodeShort : HexLiteralKind

  A \u prefix. When used without brackets, this form is limited to four digits.

def Syntax.AstItems.HexLiteralKind.digits : HexLiteralKind → Nat

Equations

• Syntax.AstItems.HexLiteralKind.x.digits = 1
• Syntax.AstItems.HexLiteralKind.X.digits = 2
• Syntax.AstItems.HexLiteralKind.UnicodeShort.digits = 4

inductive Syntax.AstItems.LiteralKind : Type

The kind of a single literal expression.

• Verbatim : LiteralKind

  The literal is written verbatim, e.g., a or ☃.

• Hex : HexLiteralKind → LiteralKind

  The literal is written as a hex code with a fixed number of digits like '\u0061'

• HexBrace : HexLiteralKind → LiteralKind

  The literal is written as a hex code with a bracketed number of digits. The only restriction is that the bracketed hex code must refer to a valid Unicode scalar value.

def Syntax.AstItems.LiteralKind.toString : LiteralKind → String

Equations

• Syntax.AstItems.LiteralKind.Verbatim.toString = "Verbatim"
• (Syntax.AstItems.LiteralKind.Hex Syntax.AstItems.HexLiteralKind.x).toString = "Hex x"
• (Syntax.AstItems.LiteralKind.Hex Syntax.AstItems.HexLiteralKind.X).toString = "Hex X"
• (Syntax.AstItems.LiteralKind.Hex Syntax.AstItems.HexLiteralKind.UnicodeShort).toString = "Hex UnicodeShort"
• (Syntax.AstItems.LiteralKind.HexBrace Syntax.AstItems.HexLiteralKind.x).toString = "HexBrace x"
• (Syntax.AstItems.LiteralKind.HexBrace Syntax.AstItems.HexLiteralKind.X).toString = "HexBrace X"
• (Syntax.AstItems.LiteralKind.HexBrace Syntax.AstItems.HexLiteralKind.UnicodeShort).toString = "HexBrace UnicodeShort"

instance Syntax.AstItems.instToStringLiteralKind : ToString LiteralKind

Equations

• Syntax.AstItems.instToStringLiteralKind = { toString := Syntax.AstItems.LiteralKind.toString }

structure Syntax.AstItems.Literal : Type

A single character literal, which includes escape sequences.

• span : Substring

  The span of this literal.

• kind : LiteralKind

  The kind of this literal.

• c : Char

  The Unicode scalar value corresponding to this literal.

def Syntax.AstItems.spanToString (span : Substring) : String

Equations

• Syntax.AstItems.spanToString span = toString "(" ++ toString span.str ++ toString "," ++ toString span.startPos ++ toString "," ++ toString span.stopPos ++ toString ")"

def Syntax.AstItems.Literal.toString (lit : Literal) : String

Equations

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

def Syntax.AstItems.Literal.toLiteral (c : Char) (p : String) (f t : String.Pos) : Literal

Equations

• Syntax.AstItems.Literal.toLiteral c p f t = { span := { str := p, startPos := f, stopPos := t }, kind := Syntax.AstItems.LiteralKind.Verbatim, c := c }

instance Syntax.AstItems.instToStringLiteral : ToString Literal

Equations

• Syntax.AstItems.instToStringLiteral = { toString := Syntax.AstItems.Literal.toString }

structure Syntax.AstItems.BackRef : Type

A backrefence to a capturung group.

• span : Substring

  The span of this backrefence.

• n : Nat

  number of the capturung group.

def Syntax.AstItems.BackRef.toString (br : BackRef) : String

Equations

• br.toString = toString "Backrefence " ++ toString (Syntax.AstItems.spanToString br.span) ++ toString " '" ++ toString br.n ++ toString "'"

instance Syntax.AstItems.instToStringBackRef : ToString BackRef

Equations

• Syntax.AstItems.instToStringBackRef = { toString := Syntax.AstItems.BackRef.toString }

inductive Syntax.AstItems.RepetitionRange : Type

A range repetition operator.

• Exactly : Nat → RepetitionRange

  {m}

• AtLeast : Nat → RepetitionRange

  {m,}

• Bounded : Nat → Nat → RepetitionRange

  {m,n}

def Syntax.AstItems.RepetitionRange.toString : RepetitionRange → String

Equations

• (Syntax.AstItems.RepetitionRange.Exactly n).toString = toString "Exactly " ++ toString n ++ toString ""
• (Syntax.AstItems.RepetitionRange.AtLeast n).toString = toString "AtLeast " ++ toString n ++ toString ""
• (Syntax.AstItems.RepetitionRange.Bounded m n).toString = toString "Bounded " ++ toString m ++ toString "," ++ toString n ++ toString ""

instance Syntax.AstItems.instToStringRepetitionRange : ToString RepetitionRange

Equations

• Syntax.AstItems.instToStringRepetitionRange = { toString := Syntax.AstItems.RepetitionRange.toString }

inductive Syntax.AstItems.RepetitionKind : Type

The kind of a repetition operator.

• ZeroOrOne : RepetitionKind

  ?

• ZeroOrMore : RepetitionKind

  *

• OneOrMore : RepetitionKind

  +

• Range : RepetitionRange → RepetitionKind

def Syntax.AstItems.RepetitionKind.toString : RepetitionKind → String

Equations

• Syntax.AstItems.RepetitionKind.ZeroOrOne.toString = "?"
• Syntax.AstItems.RepetitionKind.ZeroOrMore.toString = "*"
• Syntax.AstItems.RepetitionKind.OneOrMore.toString = "+"
• (Syntax.AstItems.RepetitionKind.Range r).toString = toString "Range " ++ toString r ++ toString ""

instance Syntax.AstItems.instToStringRepetitionKind : ToString RepetitionKind

Equations

• Syntax.AstItems.instToStringRepetitionKind = { toString := Syntax.AstItems.RepetitionKind.toString }

structure Syntax.AstItems.RepetitionOp : Type

The repetition operator itself.

• span : Substring

  The span of this Repetition .

• kind : RepetitionKind

  The kind of this Repetition .

def Syntax.AstItems.RepetitionOp.toString (r : RepetitionOp) : String

Equations

• r.toString = toString "RepetitionOp " ++ toString (Syntax.AstItems.spanToString r.span) ++ toString " " ++ toString r.kind ++ toString ""

instance Syntax.AstItems.instToStringRepetitionOp : ToString RepetitionOp

Equations

• Syntax.AstItems.instToStringRepetitionOp = { toString := Syntax.AstItems.RepetitionOp.toString }

structure Syntax.AstItems.ClassSetRange : Type

A single character class range in a set.

• span : Substring

  The span of this range.

• start : Literal

  The start of this range.

• end : Literal

  The end of this range.

• isLe : self.start.c ≤ self.end.c

  assertion

def Syntax.AstItems.ClassSetRange.toString (r : ClassSetRange) : String

Equations

• r.toString = toString "ClassSetRange " ++ toString (Syntax.AstItems.spanToString r.span) ++ toString " " ++ toString r.start ++ toString " " ++ toString r.end ++ toString ""

instance Syntax.AstItems.instToStringClassSetRange : ToString ClassSetRange

Equations

• Syntax.AstItems.instToStringClassSetRange = { toString := Syntax.AstItems.ClassSetRange.toString }

inductive Syntax.AstItems.Flag : Type

A single flag.

• CaseInsensitive : Flag

  i

• MultiLine : Flag

  m

• DotMatchesNewLine : Flag

  s

• SwapGreed : Flag

  U

• Unicode : Flag

  u

• CRLF : Flag

  R

• Extended : Flag

  x

instance Syntax.AstItems.instToStringFlag : ToString Flag

Equations

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

inductive Syntax.AstItems.FlagsItemKind : Type

The kind of an item in a group of flags.

• Negation : FlagsItemKind

  A negation operator applied to all subsequent flags in the enclosing group.

• Flag : AstItems.Flag → FlagsItemKind

  A single flag in a group.

instance Syntax.AstItems.instToStringFlagsItemKind : ToString FlagsItemKind

Equations

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

structure Syntax.AstItems.FlagsItem : Type

A single item in a group of flags.

• span : Substring

  The span of this item.

• kind : FlagsItemKind

  The kind of this item.

instance Syntax.AstItems.instToStringFlagsItem : ToString FlagsItem

Equations

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

structure Syntax.AstItems.Flags : Type

A group of flags.

• span : Substring

  The span of this item.

• items : Array FlagsItem

  The kind of this item.

instance Syntax.AstItems.instToStringFlags : ToString Flags

Equations

• Syntax.AstItems.instToStringFlags = { toString := fun (flags : Syntax.AstItems.Flags) => toString "Flags " ++ toString flags.items ++ toString "" }

inductive Syntax.AstItems.LookaroundKind : Type

The kind of a Lookaround.

• PositiveLookahead : LookaroundKind
• NegativeLookahead : LookaroundKind
• PositiveLookbehind : Nat → LookaroundKind
• NegativeLookbehind : Nat → LookaroundKind

instance Syntax.AstItems.instToStringLookaroundKind : ToString LookaroundKind

Equations

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

inductive Syntax.AstItems.GroupKind : Type

The kind of a group.

• CaptureIndex : Nat → Option String → GroupKind
• NonCapturing : Flags → GroupKind
• Lookaround : LookaroundKind → GroupKind

def Syntax.AstItems.GroupKind.toString : GroupKind → String

Equations

• (Syntax.AstItems.GroupKind.CaptureIndex i s).toString = toString "CaptureIndex " ++ toString i ++ toString " name " ++ toString s ++ toString ""
• (Syntax.AstItems.GroupKind.NonCapturing flags).toString = toString "NonCapturing " ++ toString flags ++ toString ""
• (Syntax.AstItems.GroupKind.Lookaround kind).toString = toString "Lookaround " ++ toString kind ++ toString ""

instance Syntax.AstItems.instToStringGroupKind : ToString GroupKind

Equations

• Syntax.AstItems.instToStringGroupKind = { toString := Syntax.AstItems.GroupKind.toString }

inductive Syntax.AstItems.ClassUnicodeOpKind : Type

The type of op used in a Unicode character class.

• Equal : ClassUnicodeOpKind

instance Syntax.AstItems.instToStringClassUnicodeOpKind : ToString ClassUnicodeOpKind

Equations

• Syntax.AstItems.instToStringClassUnicodeOpKind = { toString := fun (v : Syntax.AstItems.ClassUnicodeOpKind) => match v with | Syntax.AstItems.ClassUnicodeOpKind.Equal => "Equal" }

inductive Syntax.AstItems.ClassUnicodeKind : Type

The available forms of Unicode character classes.

• OneLetter : Char → ClassUnicodeKind

  A one letter abbreviated class, e.g., \pN.

• Named : String → ClassUnicodeKind

  A binary property, general category or script. The string may be empty.

• NamedValue (op : ClassUnicodeOpKind) (n v : String) : ClassUnicodeKind

  A property name and an associated value.

def Syntax.AstItems.ClassUnicodeKind.toString : ClassUnicodeKind → String

Equations

• (Syntax.AstItems.ClassUnicodeKind.OneLetter c).toString = toString "OneLetter '" ++ toString c ++ toString "'"
• (Syntax.AstItems.ClassUnicodeKind.Named s).toString = toString "Named '" ++ toString s ++ toString "'"
• (Syntax.AstItems.ClassUnicodeKind.NamedValue op n v).toString = toString "NamedValue " ++ toString op ++ toString " " ++ toString n ++ toString " " ++ toString v ++ toString ""

instance Syntax.AstItems.instToStringClassUnicodeKind : ToString ClassUnicodeKind

Equations

• Syntax.AstItems.instToStringClassUnicodeKind = { toString := Syntax.AstItems.ClassUnicodeKind.toString }

structure Syntax.AstItems.ClassUnicode : Type

A Unicode character class.

• span : Substring

  The span of this class.

• negated : Bool

  is class negated.

• kind : ClassUnicodeKind

  The kind of Unicode class.

instance Syntax.AstItems.instToStringClassUnicode : ToString ClassUnicode

Equations

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

inductive Syntax.AstItems.AssertionKind : Type

An assertion kind.

• StartLine : AssertionKind

  ^

• EndLine : AssertionKind

  $

• EndLineWithOptionalLF : AssertionKind

  $ pcre flavor

• StartText : AssertionKind

  \A

• EndText : AssertionKind

  \z

• EndTextWithOptionalLF : AssertionKind

  \Z pcre flavor

• WordBoundary : AssertionKind

  \b

• NotWordBoundary : AssertionKind

  \B

• WordBoundaryStart : AssertionKind

  \b{start}

• WordBoundaryEnd : AssertionKind

  \b{end}

• WordBoundaryStartHalf : AssertionKind

  \b{start-half}

• WordBoundaryEndHalf : AssertionKind

  \b{end-half}

• PreviousMatch : AssertionKind

  \G

• ClearMatches : AssertionKind

  \K

def Syntax.AstItems.AssertionKind.toString : AssertionKind → String

Equations

• Syntax.AstItems.AssertionKind.StartLine.toString = toString "StartLine"
• Syntax.AstItems.AssertionKind.EndLine.toString = toString "EndLine"
• Syntax.AstItems.AssertionKind.EndLineWithOptionalLF.toString = toString "EndLineWithOptionalLF"
• Syntax.AstItems.AssertionKind.StartText.toString = toString "StartText"
• Syntax.AstItems.AssertionKind.EndText.toString = toString "EndText"
• Syntax.AstItems.AssertionKind.EndTextWithOptionalLF.toString = toString "EndTextWithOptionalLF"
• Syntax.AstItems.AssertionKind.WordBoundary.toString = toString "WordBoundary"
• Syntax.AstItems.AssertionKind.NotWordBoundary.toString = toString "NotWordBoundary"
• Syntax.AstItems.AssertionKind.WordBoundaryStart.toString = toString "WordBoundaryStart"
• Syntax.AstItems.AssertionKind.WordBoundaryEnd.toString = toString "WordBoundaryEnd"
• Syntax.AstItems.AssertionKind.WordBoundaryStartHalf.toString = toString "WordBoundaryStartHalf"
• Syntax.AstItems.AssertionKind.WordBoundaryEndHalf.toString = toString "WordBoundaryEndHalf"
• Syntax.AstItems.AssertionKind.PreviousMatch.toString = toString "PreviousMatch"
• Syntax.AstItems.AssertionKind.ClearMatches.toString = toString "ClearMatches"

instance Syntax.AstItems.instToStringAssertionKind : ToString AssertionKind

Equations

• Syntax.AstItems.instToStringAssertionKind = { toString := Syntax.AstItems.AssertionKind.toString }

structure Syntax.AstItems.Assertion : Type

A single zero-width assertion.

• span : Substring

  The span of this assertion.

• kind : AssertionKind

  The assertion kind.

instance Syntax.AstItems.instToStringAssertion : ToString Assertion

Equations

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

inductive Syntax.AstItems.ClassAsciiKind : Type

The available ASCII character classes.

• Alnum : ClassAsciiKind

  [0-9A-Za-z]

• Alpha : ClassAsciiKind

  [A-Za-z]

• Ascii : ClassAsciiKind

  [\x00-\x7F]

• Blank : ClassAsciiKind

  [ \t]

• Cntrl : ClassAsciiKind

  [\x00-\x1F\x7F]

• Digit : ClassAsciiKind

  [0-9]

• Graph : ClassAsciiKind

  [!-~]

• Lower : ClassAsciiKind

  [a-z]

• Print : ClassAsciiKind

  [ -~]

• Punct : ClassAsciiKind

  ...

• Space : ClassAsciiKind

  [\t\n\v\f\r ]

• Upper : ClassAsciiKind

  [A-Z]

• Word : ClassAsciiKind

  [0-9A-Za-z_]

• Xdigit : ClassAsciiKind

  [0-9A-Fa-f]

instance Syntax.AstItems.instToStringClassAsciiKind : ToString ClassAsciiKind

Equations

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

def Syntax.AstItems.ClassAsciiKind.from_name (name : String) : Option ClassAsciiKind

Equations

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

structure Syntax.AstItems.ClassAscii : Type

An ASCII character class.

• span : Substring

  The span of this assertion.

• kind : ClassAsciiKind

  The kind of ASCII class.

• negated : Bool

  Whether the class is negated or not

instance Syntax.AstItems.instToStringClassAscii : ToString ClassAscii

Equations

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

inductive Syntax.AstItems.ClassPerlKind : Type

The available Perl character classes.

• Digit : ClassPerlKind

  Decimal numbers.

• Space : ClassPerlKind

  Whitespace.

• Word : ClassPerlKind

  Word characters.

• Newline : ClassPerlKind

  Newline.

• VerticalSpace : ClassPerlKind

  Whitespace.

• HorizontalSpace : ClassPerlKind

  Whitespace.

instance Syntax.AstItems.instToStringClassPerlKind : ToString ClassPerlKind

Equations

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

structure Syntax.AstItems.ClassPerl : Type

A Perl character class.

• span : Substring

  The span of this assertion.

• kind : ClassPerlKind

  The kind of Perl class.

• negated : Bool

  Whether the class is negated or not

instance Syntax.AstItems.instToStringClassPerl : ToString ClassPerl

Equations

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

inductive Syntax.AstItems.Repetition : Type

A repetition operation applied to a regular expression.

• mk (span : Substring) (op : RepetitionOp) (greedy possessive : Bool) (ast : Ast) : Repetition

inductive Syntax.AstItems.Group : Type

A grouped regular expression.

• mk (span : Substring) (kind : GroupKind) (ast : Ast) : Group

inductive Syntax.AstItems.SetFlags : Type

A group of flags that is not applied to a particular regular expression.

• mk (span : Substring) (flags : Flags) : SetFlags

inductive Syntax.AstItems.Primitive : Type

A primitive is an expression with no sub-expressions.

• Literal : AstItems.Literal → Primitive
• BackRef : AstItems.BackRef → Primitive
• Dot : Substring → Primitive
• Assertion : AstItems.Assertion → Primitive
• Unicode : ClassUnicode → Primitive
• Perl : ClassPerl → Primitive

inductive Syntax.AstItems.ClassSetUnion : Type

A union of items inside a character class set.

• mk (span : Substring) (items : Array ClassSetItem) : ClassSetUnion

inductive Syntax.AstItems.ClassSetItem : Type

A single component of a character class set.

• Empty : Substring → ClassSetItem

  An empty item.

• Literal : AstItems.Literal → ClassSetItem

  A single literal.

• Range : ClassSetRange → ClassSetItem

  A range between two literals.

• Ascii : ClassAscii → ClassSetItem

  An ASCII character class, e.g., [:alnum:] or [:punct:].

• Unicode : ClassUnicode → ClassSetItem

  A Unicode character class, e.g., \pL or \p{Greek}.

• Perl : ClassPerl → ClassSetItem

  A perl character class, e.g., \d or \W.

• Bracketed : ClassBracketed → ClassSetItem

  A bracketed character class set, which may contain zero or more character ranges and/or zero or more nested classes. e.g., [a-zA-Z\pL].

• Union : ClassSetUnion → ClassSetItem

  A union of items.

inductive Syntax.AstItems.ClassSetBinaryOpKind : Type

The type of a Unicode character class set operation.

• Intersection : ClassSetBinaryOpKind

  The intersection of two sets, e.g., \pN&&[a-z].

• Difference : ClassSetBinaryOpKind

  The difference of two sets, e.g., \pN--[0-9].

• SymmetricDifference : ClassSetBinaryOpKind

  The symmetric difference of two sets. The symmetric difference is the set of elements belonging to one but not both sets.

inductive Syntax.AstItems.ClassSetBinaryOp : Type

A Unicode character class set operation.

• mk (span : Substring) (kind : ClassSetBinaryOpKind) (lhs rhs : ClassSet) : ClassSetBinaryOp

inductive Syntax.AstItems.ClassSet : Type

A character class set.

• Item : ClassSetItem → ClassSet

  An item, which can be a single literal, range, nested character class or a union of items.

• BinaryOp : ClassSetBinaryOp → ClassSet

  A single binary operation (i.e., &&, -- or ~~).

inductive Syntax.AstItems.ClassBracketed : Type

A bracketed character class, e.g., [a-z0-9].

• mk (span : Substring) (negated : Bool) (kind : ClassSet) : ClassBracketed

inductive Syntax.AstItems.Alternation : Type

An alternation of regular expressions.

• mk (span : Substring) (asts : Array Ast) : Alternation

inductive Syntax.AstItems.Concat : Type

A concatenation of regular expressions.

• mk (span : Substring) (asts : Array Ast) : Concat

inductive Syntax.AstItems.Ast : Type

An abstract syntax tree for a single regular expression.

• Empty : Ast

  An empty regex that matches everything.

• Flags : SetFlags → Ast

  A set of flags, e.g., (?is).

• Literal : AstItems.Literal → Ast

  A single character literal, which includes escape sequences.

• BackRef : AstItems.BackRef → Ast

  A backrefence to a capturung group.

• Dot : Substring → Ast

  The "any character" class.

• Assertion : AstItems.Assertion → Ast

  A single zero-width assertion.

• ClassUnicode : AstItems.ClassUnicode → Ast

  A single Unicode character class, e.g., \pL or \p{Greek}.

• ClassPerl : AstItems.ClassPerl → Ast

  A single perl character class, e.g., \d or \W.

• ClassBracketed : AstItems.ClassBracketed → Ast

  A single bracketed character class set, which may contain zero or more character range.

• Repetition : AstItems.Repetition → Ast

  A repetition operator applied to an arbitrary regular expression.

• Alternation : AstItems.Alternation → Ast

  An alternation of regular expressions.

• Group : AstItems.Group → Ast

  A grouped regular expression.

• Concat : AstItems.Concat → Ast

  A concatenation of regular expressions.

instance Syntax.AstItems.instInhabitedAst : Inhabited Ast

Equations

• Syntax.AstItems.instInhabitedAst = { default := Syntax.AstItems.Ast.Empty }

def Syntax.AstItems.ClassSetUnion.items (union : ClassSetUnion) : Array ClassSetItem

Equations

• (Syntax.AstItems.ClassSetUnion.mk span items).items = items

def Syntax.AstItems.ClassSetUnion.into_item (union : ClassSetUnion) : ClassSetItem

Return this union as a character class set item.

Equations

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

def Syntax.AstItems.ClassBracketed.span (cls : ClassBracketed) : Substring

Equations

• (Syntax.AstItems.ClassBracketed.mk span negated kind).span = span

def Syntax.AstItems.ClassBracketed.negate (cls : ClassBracketed) : Bool

Equations

• (Syntax.AstItems.ClassBracketed.mk span negated kind).negate = negated

def Syntax.AstItems.Concat.span (concat : Concat) : Substring

Equations

• (Syntax.AstItems.Concat.mk span asts).span = span

def Syntax.AstItems.Concat.asts (concat : Concat) : Array Ast

Equations

• (Syntax.AstItems.Concat.mk span asts).asts = asts

theorem Syntax.AstItems.Concat.sizeOfAstsOfConcat (concat : Concat) : sizeOf concat.asts < sizeOf concat

def Syntax.AstItems.Concat.into_ast (concat : Concat) : Ast

Equations

• concat.into_ast = match concat.asts.size with | 0 => Syntax.AstItems.Ast.Empty | 1 => concat.asts[0]! | x => Syntax.AstItems.Ast.Concat concat

def Syntax.AstItems.Alternation.asts (concat : Alternation) : Array Ast

Equations

• (Syntax.AstItems.Alternation.mk span asts).asts = asts

theorem Syntax.AstItems.Alternation.sizeOfAstsOfAlternation (alt : Alternation) : sizeOf alt.asts < sizeOf alt

def Syntax.AstItems.Alternation.into_ast (alt : Alternation) : Ast

Equations

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

def Syntax.AstItems.Primitive.into_ast (p : Primitive) : Ast

Equations

• (Syntax.AstItems.Primitive.Literal lit).into_ast = Syntax.AstItems.Ast.Literal lit
• (Syntax.AstItems.Primitive.BackRef n).into_ast = Syntax.AstItems.Ast.BackRef n
• (Syntax.AstItems.Primitive.Dot span).into_ast = Syntax.AstItems.Ast.Dot span
• (Syntax.AstItems.Primitive.Assertion a).into_ast = Syntax.AstItems.Ast.Assertion a
• (Syntax.AstItems.Primitive.Unicode cls).into_ast = Syntax.AstItems.Ast.ClassUnicode cls
• (Syntax.AstItems.Primitive.Perl cls).into_ast = Syntax.AstItems.Ast.ClassPerl cls

def Syntax.AstItems.Primitive.into_class_set_item (p : Primitive) : Except String ClassSetItem

Equations

• (Syntax.AstItems.Primitive.Literal lit).into_class_set_item = Except.ok (Syntax.AstItems.ClassSetItem.Literal lit)
• (Syntax.AstItems.Primitive.Perl cls).into_class_set_item = Except.ok (Syntax.AstItems.ClassSetItem.Perl cls)
• (Syntax.AstItems.Primitive.Unicode cls).into_class_set_item = Except.ok (Syntax.AstItems.ClassSetItem.Unicode cls)
• p.into_class_set_item = Except.error "into_class_set_item, unexpected entry"

def Syntax.AstItems.Primitive.into_class_literal (p : Primitive) : Except String AstItems.Literal

Equations

• (Syntax.AstItems.Primitive.Literal lit).into_class_literal = Except.ok lit
• (Syntax.AstItems.Primitive.Perl a).into_class_literal = Except.error "escape sequence unexpected in range"
• p.into_class_literal = Except.error "into_class_literal, unexpected entry"

def Syntax.AstItems.Group.kind (g : Group) : GroupKind

Equations

• (Syntax.AstItems.Group.mk span kind ast).kind = kind

def Syntax.AstItems.Group.ast (g : Group) : Ast

Equations

• (Syntax.AstItems.Group.mk span kind ast).ast = ast

theorem Syntax.AstItems.Group.sizeOfAstOfGroup (g : Group) : sizeOf g.ast < sizeOf g

def Syntax.AstItems.ClassSetBinaryOp.kind (cls : ClassSetBinaryOp) : ClassSetBinaryOpKind

Equations

• (Syntax.AstItems.ClassSetBinaryOp.mk span kind lhs rhs).kind = kind

instance Syntax.AstItems.instToStringSetFlags : ToString SetFlags

Equations

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

@[irreducible]

def Syntax.AstItems.ClassSetItem.toStringClassSetUnion (r : ClassSetUnion) (col : Nat) : String

Equations

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

@[irreducible]

def Syntax.AstItems.ClassSetItem.toStringClassSetItem (r : ClassSetItem) (col : Nat) : String

Equations

• One or more equations did not get rendered due to their size.
• (Syntax.AstItems.ClassSetItem.Empty a).toStringClassSetItem col = toString "ItemEmpty"
• (Syntax.AstItems.ClassSetItem.Literal lit).toStringClassSetItem col = toString "Item " ++ toString lit ++ toString ""
• (Syntax.AstItems.ClassSetItem.Range range).toStringClassSetItem col = toString "Item " ++ toString range ++ toString ""
• (Syntax.AstItems.ClassSetItem.Ascii cls).toStringClassSetItem col = toString "Item " ++ toString cls ++ toString ""
• (Syntax.AstItems.ClassSetItem.Perl cls).toStringClassSetItem col = toString "Item " ++ toString cls ++ toString ""
• (Syntax.AstItems.ClassSetItem.Unicode cls).toStringClassSetItem col = toString "Item " ++ toString cls ++ toString ""
• (Syntax.AstItems.ClassSetItem.Union union).toStringClassSetItem col = toString "Item Union " ++ toString (Syntax.AstItems.ClassSetItem.toStringClassSetUnion union col) ++ toString ""

instance Syntax.AstItems.instToStringClassSetUnion : ToString ClassSetUnion

Equations

• Syntax.AstItems.instToStringClassSetUnion = { toString := fun (union : Syntax.AstItems.ClassSetUnion) => Syntax.AstItems.ClassSetItem.toStringClassSetUnion union 0 }

instance Syntax.AstItems.instToStringClassSetItem : ToString ClassSetItem

Equations

• Syntax.AstItems.instToStringClassSetItem = { toString := fun (item : Syntax.AstItems.ClassSetItem) => item.toStringClassSetItem 0 }

def Syntax.AstItems.ClassSetBinaryOpKind.toString (r : ClassSetBinaryOpKind) : String

Equations

• Syntax.AstItems.ClassSetBinaryOpKind.Intersection.toString = toString "Intersection"
• Syntax.AstItems.ClassSetBinaryOpKind.Difference.toString = toString "Difference"
• Syntax.AstItems.ClassSetBinaryOpKind.SymmetricDifference.toString = toString "SymmetricDifference"

def Syntax.AstItems.ClassSet.toString (r : ClassSet) (col : Nat) : String

Equations

• One or more equations did not get rendered due to their size.
• (Syntax.AstItems.ClassSet.Item item).toString col = toString "ClassSet " ++ toString (item.toStringClassSetItem (col + 2)) ++ toString ""

instance Syntax.AstItems.instToStringClassSet : ToString ClassSet

Equations

• Syntax.AstItems.instToStringClassSet = { toString := fun (s : Syntax.AstItems.ClassSet) => s.toString 0 }

def Syntax.AstItems.Repetition.op (rep : Repetition) : RepetitionOp

Equations

• (Syntax.AstItems.Repetition.mk span op greedy possessive ast).op = op

def Syntax.AstItems.Repetition.greedy (rep : Repetition) : Bool

Equations

• (Syntax.AstItems.Repetition.mk span op greedy possessive ast).greedy = greedy

def Syntax.AstItems.Repetition.possessive (rep : Repetition) : Bool

Equations

• (Syntax.AstItems.Repetition.mk span op greedy possessive ast).possessive = possessive

def Syntax.AstItems.Repetition.ast (rep : Repetition) : Ast

Equations

• (Syntax.AstItems.Repetition.mk span op greedy possessive ast).ast = ast

theorem Syntax.AstItems.Repetition.sizeOfAstOfRepetition (rep : Repetition) : sizeOf rep.ast < sizeOf rep

def Syntax.AstItems.span (ast : Ast) : Substring

Equations

• Syntax.AstItems.span Syntax.AstItems.Ast.Empty = default
• Syntax.AstItems.span (Syntax.AstItems.Ast.Flags (Syntax.AstItems.SetFlags.mk span flags)) = span
• Syntax.AstItems.span (Syntax.AstItems.Ast.Literal lit) = lit.span
• Syntax.AstItems.span (Syntax.AstItems.Ast.BackRef br) = br.span
• Syntax.AstItems.span (Syntax.AstItems.Ast.Dot span) = span
• Syntax.AstItems.span (Syntax.AstItems.Ast.Assertion { span := span, kind := kind }) = span
• Syntax.AstItems.span (Syntax.AstItems.Ast.ClassUnicode cls) = cls.span
• Syntax.AstItems.span (Syntax.AstItems.Ast.ClassPerl cls) = cls.span
• Syntax.AstItems.span (Syntax.AstItems.Ast.ClassBracketed (Syntax.AstItems.ClassBracketed.mk span negated kind)) = span
• Syntax.AstItems.span (Syntax.AstItems.Ast.Repetition (Syntax.AstItems.Repetition.mk span op greedy possessive ast_2)) = span
• Syntax.AstItems.span (Syntax.AstItems.Ast.Alternation (Syntax.AstItems.Alternation.mk span asts)) = span
• Syntax.AstItems.span (Syntax.AstItems.Ast.Group (Syntax.AstItems.Group.mk span kind ast_2)) = span
• Syntax.AstItems.span (Syntax.AstItems.Ast.Concat concat) = concat.span

@[irreducible]

def Syntax.AstItems.toString (ast : Ast) (col : Nat) : String

Equations

• One or more equations did not get rendered due to their size.
• Syntax.AstItems.toString Syntax.AstItems.Ast.Empty col = toString "Empty"
• Syntax.AstItems.toString (Syntax.AstItems.Ast.Flags (Syntax.AstItems.SetFlags.mk span flags)) col = toString "Flags " ++ toString flags ++ toString ""
• Syntax.AstItems.toString (Syntax.AstItems.Ast.Literal lit) col = toString "" ++ toString lit ++ toString ""
• Syntax.AstItems.toString (Syntax.AstItems.Ast.BackRef br) col = toString "" ++ toString br ++ toString ""
• Syntax.AstItems.toString (Syntax.AstItems.Ast.Dot span) col = toString "Dot " ++ toString (Syntax.AstItems.spanToString span) ++ toString ""
• Syntax.AstItems.toString (Syntax.AstItems.Ast.Assertion a) col = toString "Assertion " ++ toString a ++ toString ""
• Syntax.AstItems.toString (Syntax.AstItems.Ast.ClassUnicode cls) col = toString "ClassUnicode " ++ toString cls ++ toString ""
• Syntax.AstItems.toString (Syntax.AstItems.Ast.ClassPerl cls) col = toString "ClassPerl " ++ toString cls ++ toString ""

instance Syntax.AstItems.instToStringAst : ToString Ast

Equations

• Syntax.AstItems.instToStringAst = { toString := fun (ast : Syntax.AstItems.Ast) => Syntax.AstItems.toString ast 0 }

partial def Syntax.AstItems.find (ast : Ast) (p : Ast → Bool) : Option Ast

@[irreducible]

def Syntax.AstItems.get_fixed_width (pattern : String) (ast : Ast) : Except String Nat

Equations

• One or more equations did not get rendered due to their size.
• Syntax.AstItems.get_fixed_width pattern (Syntax.AstItems.Ast.Literal a) = pure 1
• Syntax.AstItems.get_fixed_width pattern (Syntax.AstItems.Ast.Dot a) = pure 1
• Syntax.AstItems.get_fixed_width pattern (Syntax.AstItems.Ast.ClassBracketed a) = pure 1
• Syntax.AstItems.get_fixed_width pattern (Syntax.AstItems.Ast.ClassUnicode a) = pure 1
• Syntax.AstItems.get_fixed_width pattern (Syntax.AstItems.Ast.ClassPerl a) = pure 1
• Syntax.AstItems.get_fixed_width pattern (Syntax.AstItems.Ast.Assertion a) = pure 0
• Syntax.AstItems.get_fixed_width pattern (Syntax.AstItems.Ast.Flags a) = pure 0
• Syntax.AstItems.get_fixed_width pattern (Syntax.AstItems.Ast.Repetition rep) = throw (Syntax.AstItems.toError pattern Syntax.AstItems.ErrorKind.FixedWidtExcpected)
• Syntax.AstItems.get_fixed_width pattern (Syntax.AstItems.Ast.Group (Syntax.AstItems.Group.mk span (Syntax.AstItems.GroupKind.Lookaround a) ast_2)) = pure 0
• Syntax.AstItems.get_fixed_width pattern ast = throw (Syntax.AstItems.toError pattern Syntax.AstItems.ErrorKind.FixedWidtExcpected)

def Syntax.AstItems.checkBackRefence (b : Nat) (ast : Ast) : Except String Bool

Equations

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

@[irreducible]

def Syntax.AstItems.checkBackRefences (b : Nat) (ast : Ast) : Except String Bool

capture groups with a backreference should have fixed width

Equations

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