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: Syntax.AstItems.ErrorKind

  Backrefence invalid.

• CaptureLimitExceeded: Syntax.AstItems.ErrorKind

  The capturing group limit was exceeded.

• ClassEscapeInvalid: Syntax.AstItems.ErrorKind

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

• ClassRangeInvalid: Syntax.AstItems.ErrorKind

  An invalid character class range was found.

• ClassRangeLiteral: Syntax.AstItems.ErrorKind

  An invalid range boundary was found in a character class.

• ClassUnclosed: Syntax.AstItems.ErrorKind

  An opening [ was found with no corresponding closing ].

• DecimalInvalid: Syntax.AstItems.ErrorKind

  An invalid decimal number was given where one was expected.

• EndQuoteWithoutOpenQuote: Syntax.AstItems.ErrorKind

  End quote without a corresponding open quote.

• EscapeHexEmpty: Syntax.AstItems.ErrorKind

  A bracketed hex literal was empty.

• EscapeHexInvalid: Syntax.AstItems.ErrorKind

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

• EscapeHexInvalidDigit: Syntax.AstItems.ErrorKind

  An invalid hexadecimal digit was found.

• EscapeUnexpectedEof: Syntax.AstItems.ErrorKind

  EOF was found before an escape sequence was completed.

• EscapeUnrecognized: Syntax.AstItems.ErrorKind

  An unrecognized escape sequence.

• FixedWidtExcpected: Syntax.AstItems.ErrorKind

  Fixed width in look behind

• FlagDanglingNegation: Syntax.AstItems.ErrorKind

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

• FlagDuplicate: Syntax.AstItems.ErrorKind

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

• FlagRepeatedNegation: Syntax.AstItems.ErrorKind

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

• FlagUnexpectedEof: Syntax.AstItems.ErrorKind

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

• FlagUnrecognized: Syntax.AstItems.ErrorKind

  Unrecognized flag, e.g., a.

• GroupNameDuplicate: Syntax.AstItems.ErrorKind

  A duplicate capture name was found.

• GroupNameEmpty: Syntax.AstItems.ErrorKind

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

• GroupNameInvalid: Syntax.AstItems.ErrorKind

  An invalid character was seen for a capture group name.

• GroupNameNotFound: Syntax.AstItems.ErrorKind

  A capture group name is not found of a backreference.

• GroupNameUnexpectedEof: Syntax.AstItems.ErrorKind

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

• GroupUnclosed: Syntax.AstItems.ErrorKind

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

• GroupUnopened: Syntax.AstItems.ErrorKind

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

• NestLimitExceeded: Syntax.AstItems.ErrorKind

  The nest limit was exceeded.

• RepetitionCountInvalid: Syntax.AstItems.ErrorKind

  The range provided in a counted repetition operator is invalid.

• RepetitionCountDecimalEmpty: Syntax.AstItems.ErrorKind

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

• RepetitionCountUnclosed: Syntax.AstItems.ErrorKind

  An opening { was found with no corresponding closing }.

• RepetitionMissing: Syntax.AstItems.ErrorKind

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

• RepetitionUngreedyAndPossessive: Syntax.AstItems.ErrorKind

  A repetition operator was ungreedy and possessive.

• SpecialWordBoundaryUnclosed: Syntax.AstItems.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: Syntax.AstItems.ErrorKind

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

• SpecialWordOrRepetitionUnexpectedEof: Syntax.AstItems.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: Syntax.AstItems.ErrorKind

  The Unicode class is not valid.

• UnsupportedBackreference: Syntax.AstItems.ErrorKind

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

• UnsupportedLookAround: Syntax.AstItems.ErrorKind

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

• UnkownAsciiClass: Syntax.AstItems.ErrorKind

  ClassAsci not found.

• EscapeOctalInvalid: Syntax.AstItems.ErrorKind

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

• FeatureNotImplementedSubroutines: Syntax.AstItems.ErrorKind

  Feature not implemented.

• FeatureNotImplementedFlagShorthand: Syntax.AstItems.ErrorKind

  Feature not implemented.

• FeatureNotImplementedAtomicGroup: Syntax.AstItems.ErrorKind

  Feature not implemented.

• FeatureNotImplementedConditionalExpression: Syntax.AstItems.ErrorKind

  Feature not implemented.

• FeatureNotImplementedBranchResetGroup: Syntax.AstItems.ErrorKind

  Feature not implemented.

• FeatureNotImplementedControlVerbs: Syntax.AstItems.ErrorKind

  Feature not implemented.

• FeatureNotImplementedFlagExtended: Syntax.AstItems.ErrorKind

  Feature not implemented.

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

Equations

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

instance Syntax.AstItems.instToStringErrorKind : ToString Syntax.AstItems.ErrorKind

Equations

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

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

Equations

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

def Syntax.AstItems.toErrorAt (s : String) (i : Nat) (kind : Syntax.AstItems.ErrorKind) (msg : optParam 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: Syntax.AstItems.HexLiteralKind

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

• X: Syntax.AstItems.HexLiteralKind

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

• UnicodeShort: Syntax.AstItems.HexLiteralKind

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

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

Equations

• x.digits = match x with | Syntax.AstItems.HexLiteralKind.x => 1 | Syntax.AstItems.HexLiteralKind.X => 2 | Syntax.AstItems.HexLiteralKind.UnicodeShort => 4

inductive Syntax.AstItems.LiteralKind : Type

The kind of a single literal expression.

• Verbatim: Syntax.AstItems.LiteralKind

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

• Hex: Syntax.AstItems.HexLiteralKind → Syntax.AstItems.LiteralKind

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

• HexBrace: Syntax.AstItems.HexLiteralKind → Syntax.AstItems.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 : Syntax.AstItems.LiteralKind → String

Equations

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

instance Syntax.AstItems.instToStringLiteralKind : ToString Syntax.AstItems.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 : Syntax.AstItems.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 : Syntax.AstItems.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 : String.Pos) (t : String.Pos) : Syntax.AstItems.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 Syntax.AstItems.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 : Syntax.AstItems.BackRef) : String

Equations

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

instance Syntax.AstItems.instToStringBackRef : ToString Syntax.AstItems.BackRef

Equations

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

inductive Syntax.AstItems.RepetitionRange : Type

A range repetition operator.

• Exactly: Nat → Syntax.AstItems.RepetitionRange

  {m}

• AtLeast: Nat → Syntax.AstItems.RepetitionRange

  {m,}

• Bounded: Nat → Nat → Syntax.AstItems.RepetitionRange

  {m,n}

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

Equations

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

instance Syntax.AstItems.instToStringRepetitionRange : ToString Syntax.AstItems.RepetitionRange

Equations

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

inductive Syntax.AstItems.RepetitionKind : Type

The kind of a repetition operator.

• ZeroOrOne: Syntax.AstItems.RepetitionKind

  ?

• ZeroOrMore: Syntax.AstItems.RepetitionKind

  *

• OneOrMore: Syntax.AstItems.RepetitionKind

  +

• Range: Syntax.AstItems.RepetitionRange → Syntax.AstItems.RepetitionKind

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

Equations

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

instance Syntax.AstItems.instToStringRepetitionKind : ToString Syntax.AstItems.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 : Syntax.AstItems.RepetitionKind

  The kind of this Repetition .

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

Equations

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

instance Syntax.AstItems.instToStringRepetitionOp : ToString Syntax.AstItems.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 : Syntax.AstItems.Literal

  The start of this range.

• end : Syntax.AstItems.Literal

  The end of this range.

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

  assertion

theorem Syntax.AstItems.ClassSetRange.isLe (self : Syntax.AstItems.ClassSetRange) : self.start.c ≤ self.end.c

assertion

def Syntax.AstItems.ClassSetRange.toString (r : Syntax.AstItems.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 Syntax.AstItems.ClassSetRange

Equations

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

inductive Syntax.AstItems.Flag : Type

A single flag.

• CaseInsensitive: Syntax.AstItems.Flag

  i

• MultiLine: Syntax.AstItems.Flag

  m

• DotMatchesNewLine: Syntax.AstItems.Flag

  s

• SwapGreed: Syntax.AstItems.Flag

  U

• Unicode: Syntax.AstItems.Flag

  u

• CRLF: Syntax.AstItems.Flag

  R

• Extended: Syntax.AstItems.Flag

  x

instance Syntax.AstItems.instToStringFlag : ToString Syntax.AstItems.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: Syntax.AstItems.FlagsItemKind

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

• Flag: Syntax.AstItems.Flag → Syntax.AstItems.FlagsItemKind

  A single flag in a group.

instance Syntax.AstItems.instToStringFlagsItemKind : ToString Syntax.AstItems.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 : Syntax.AstItems.FlagsItemKind

  The kind of this item.

instance Syntax.AstItems.instToStringFlagsItem : ToString Syntax.AstItems.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 Syntax.AstItems.FlagsItem

  The kind of this item.

instance Syntax.AstItems.instToStringFlags : ToString Syntax.AstItems.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: Syntax.AstItems.LookaroundKind
• NegativeLookahead: Syntax.AstItems.LookaroundKind
• PositiveLookbehind: Nat → Syntax.AstItems.LookaroundKind
• NegativeLookbehind: Nat → Syntax.AstItems.LookaroundKind

instance Syntax.AstItems.instToStringLookaroundKind : ToString Syntax.AstItems.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 → Syntax.AstItems.GroupKind
• NonCapturing: Syntax.AstItems.Flags → Syntax.AstItems.GroupKind
• Lookaround: Syntax.AstItems.LookaroundKind → Syntax.AstItems.GroupKind

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

Equations

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

instance Syntax.AstItems.instToStringGroupKind : ToString Syntax.AstItems.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: Syntax.AstItems.ClassUnicodeOpKind

instance Syntax.AstItems.instToStringClassUnicodeOpKind : ToString Syntax.AstItems.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 → Syntax.AstItems.ClassUnicodeKind

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

• Named: String → Syntax.AstItems.ClassUnicodeKind

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

• NamedValue: Syntax.AstItems.ClassUnicodeOpKind → String → String → Syntax.AstItems.ClassUnicodeKind

  A property name and an associated value.

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

Equations

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

instance Syntax.AstItems.instToStringClassUnicodeKind : ToString Syntax.AstItems.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 : Syntax.AstItems.ClassUnicodeKind

  The kind of Unicode class.

instance Syntax.AstItems.instToStringClassUnicode : ToString Syntax.AstItems.ClassUnicode

Equations

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

inductive Syntax.AstItems.AssertionKind : Type

An assertion kind.

• StartLine: Syntax.AstItems.AssertionKind

  ^

• EndLine: Syntax.AstItems.AssertionKind

  $

• EndLineWithOptionalLF: Syntax.AstItems.AssertionKind

  $ pcre flavor

• StartText: Syntax.AstItems.AssertionKind

  \A

• EndText: Syntax.AstItems.AssertionKind

  \z

• EndTextWithOptionalLF: Syntax.AstItems.AssertionKind

  \Z pcre flavor

• WordBoundary: Syntax.AstItems.AssertionKind

  \b

• NotWordBoundary: Syntax.AstItems.AssertionKind

  \B

• WordBoundaryStart: Syntax.AstItems.AssertionKind

  \b{start}

• WordBoundaryEnd: Syntax.AstItems.AssertionKind

  \b{end}

• WordBoundaryStartHalf: Syntax.AstItems.AssertionKind

  \b{start-half}

• WordBoundaryEndHalf: Syntax.AstItems.AssertionKind

  \b{end-half}

• PreviousMatch: Syntax.AstItems.AssertionKind

  \G

• ClearMatches: Syntax.AstItems.AssertionKind

  \K

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

Equations

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

instance Syntax.AstItems.instToStringAssertionKind : ToString Syntax.AstItems.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 : Syntax.AstItems.AssertionKind

  The assertion kind.

instance Syntax.AstItems.instToStringAssertion : ToString Syntax.AstItems.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: Syntax.AstItems.ClassAsciiKind

  [0-9A-Za-z]

• Alpha: Syntax.AstItems.ClassAsciiKind

  [A-Za-z]

• Ascii: Syntax.AstItems.ClassAsciiKind

  [\x00-\x7F]

• Blank: Syntax.AstItems.ClassAsciiKind

  [ \t]

• Cntrl: Syntax.AstItems.ClassAsciiKind

  [\x00-\x1F\x7F]

• Digit: Syntax.AstItems.ClassAsciiKind

  [0-9]

• Graph: Syntax.AstItems.ClassAsciiKind

  [!-~]

• Lower: Syntax.AstItems.ClassAsciiKind

  [a-z]

• Print: Syntax.AstItems.ClassAsciiKind

  [ -~]

• Punct: Syntax.AstItems.ClassAsciiKind

  ...

• Space: Syntax.AstItems.ClassAsciiKind

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

• Upper: Syntax.AstItems.ClassAsciiKind

  [A-Z]

• Word: Syntax.AstItems.ClassAsciiKind

  [0-9A-Za-z_]

• Xdigit: Syntax.AstItems.ClassAsciiKind

  [0-9A-Fa-f]

instance Syntax.AstItems.instToStringClassAsciiKind : ToString Syntax.AstItems.ClassAsciiKind

Equations

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

def Syntax.AstItems.ClassAsciiKind.from_name (name : String) : Option Syntax.AstItems.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 : Syntax.AstItems.ClassAsciiKind

  The kind of ASCII class.

• negated : Bool

  Whether the class is negated or not

instance Syntax.AstItems.instToStringClassAscii : ToString Syntax.AstItems.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: Syntax.AstItems.ClassPerlKind

  Decimal numbers.

• Space: Syntax.AstItems.ClassPerlKind

  Whitespace.

• Word: Syntax.AstItems.ClassPerlKind

  Word characters.

• Newline: Syntax.AstItems.ClassPerlKind

  Newline.

• VerticalSpace: Syntax.AstItems.ClassPerlKind

  Whitespace.

• HorizontalSpace: Syntax.AstItems.ClassPerlKind

  Whitespace.

instance Syntax.AstItems.instToStringClassPerlKind : ToString Syntax.AstItems.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 : Syntax.AstItems.ClassPerlKind

  The kind of Perl class.

• negated : Bool

  Whether the class is negated or not

instance Syntax.AstItems.instToStringClassPerl : ToString Syntax.AstItems.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: Substring → Syntax.AstItems.RepetitionOp → Bool → Bool → Syntax.AstItems.Ast → Syntax.AstItems.Repetition

inductive Syntax.AstItems.Group : Type

A grouped regular expression.

• mk: Substring → Syntax.AstItems.GroupKind → Syntax.AstItems.Ast → Syntax.AstItems.Group

inductive Syntax.AstItems.SetFlags : Type

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

• mk: Substring → Syntax.AstItems.Flags → Syntax.AstItems.SetFlags

inductive Syntax.AstItems.Primitive : Type

A primitive is an expression with no sub-expressions.

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

inductive Syntax.AstItems.ClassSetUnion : Type

A union of items inside a character class set.

• mk: Substring → Array Syntax.AstItems.ClassSetItem → Syntax.AstItems.ClassSetUnion

inductive Syntax.AstItems.ClassSetItem : Type

A single component of a character class set.

• Empty: Substring → Syntax.AstItems.ClassSetItem

  An empty item.

• Literal: Syntax.AstItems.Literal → Syntax.AstItems.ClassSetItem

  A single literal.

• Range: Syntax.AstItems.ClassSetRange → Syntax.AstItems.ClassSetItem

  A range between two literals.

• Ascii: Syntax.AstItems.ClassAscii → Syntax.AstItems.ClassSetItem

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

• Unicode: Syntax.AstItems.ClassUnicode → Syntax.AstItems.ClassSetItem

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

• Perl: Syntax.AstItems.ClassPerl → Syntax.AstItems.ClassSetItem

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

• Bracketed: Syntax.AstItems.ClassBracketed → Syntax.AstItems.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: Syntax.AstItems.ClassSetUnion → Syntax.AstItems.ClassSetItem

  A union of items.

inductive Syntax.AstItems.ClassSetBinaryOpKind : Type

The type of a Unicode character class set operation.

• Intersection: Syntax.AstItems.ClassSetBinaryOpKind

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

• Difference: Syntax.AstItems.ClassSetBinaryOpKind

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

• SymmetricDifference: Syntax.AstItems.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: Substring → Syntax.AstItems.ClassSetBinaryOpKind → Syntax.AstItems.ClassSet → Syntax.AstItems.ClassSet → Syntax.AstItems.ClassSetBinaryOp

inductive Syntax.AstItems.ClassSet : Type

A character class set.

• Item: Syntax.AstItems.ClassSetItem → Syntax.AstItems.ClassSet

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

• BinaryOp: Syntax.AstItems.ClassSetBinaryOp → Syntax.AstItems.ClassSet

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

inductive Syntax.AstItems.ClassBracketed : Type

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

• mk: Substring → Bool → Syntax.AstItems.ClassSet → Syntax.AstItems.ClassBracketed

inductive Syntax.AstItems.Alternation : Type

An alternation of regular expressions.

• mk: Substring → Array Syntax.AstItems.Ast → Syntax.AstItems.Alternation

inductive Syntax.AstItems.Concat : Type

A concatenation of regular expressions.

• mk: Substring → Array Syntax.AstItems.Ast → Syntax.AstItems.Concat

inductive Syntax.AstItems.Ast : Type

An abstract syntax tree for a single regular expression.

• Empty: Syntax.AstItems.Ast

  An empty regex that matches everything.

• Flags: Syntax.AstItems.SetFlags → Syntax.AstItems.Ast

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

• Literal: Syntax.AstItems.Literal → Syntax.AstItems.Ast

  A single character literal, which includes escape sequences.

• BackRef: Syntax.AstItems.BackRef → Syntax.AstItems.Ast

  A backrefence to a capturung group.

• Dot: Substring → Syntax.AstItems.Ast

  The "any character" class.

• Assertion: Syntax.AstItems.Assertion → Syntax.AstItems.Ast

  A single zero-width assertion.

• ClassUnicode: Syntax.AstItems.ClassUnicode → Syntax.AstItems.Ast

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

• ClassPerl: Syntax.AstItems.ClassPerl → Syntax.AstItems.Ast

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

• ClassBracketed: Syntax.AstItems.ClassBracketed → Syntax.AstItems.Ast

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

• Repetition: Syntax.AstItems.Repetition → Syntax.AstItems.Ast

  A repetition operator applied to an arbitrary regular expression.

• Alternation: Syntax.AstItems.Alternation → Syntax.AstItems.Ast

  An alternation of regular expressions.

• Group: Syntax.AstItems.Group → Syntax.AstItems.Ast

  A grouped regular expression.

• Concat: Syntax.AstItems.Concat → Syntax.AstItems.Ast

  A concatenation of regular expressions.

instance Syntax.AstItems.instInhabitedAst : Inhabited Syntax.AstItems.Ast

Equations

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

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

Equations

• union.items = match union with | Syntax.AstItems.ClassSetUnion.mk span items => items

def Syntax.AstItems.ClassSetUnion.into_item (union : Syntax.AstItems.ClassSetUnion) : Syntax.AstItems.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 : Syntax.AstItems.ClassBracketed) : Substring

Equations

• cls.span = match cls with | Syntax.AstItems.ClassBracketed.mk span negated kind => span

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

Equations

• cls.negate = match cls with | Syntax.AstItems.ClassBracketed.mk span negate kind => negate

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

Equations

• concat.span = match concat with | Syntax.AstItems.Concat.mk span asts => span

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

Equations

• concat.asts = match concat with | Syntax.AstItems.Concat.mk span asts => asts

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

def Syntax.AstItems.Concat.into_ast (concat : Syntax.AstItems.Concat) : Syntax.AstItems.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 : Syntax.AstItems.Alternation) : Array Syntax.AstItems.Ast

Equations

• concat.asts = match concat with | Syntax.AstItems.Alternation.mk span asts => asts

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• g.kind = match g with | Syntax.AstItems.Group.mk span kind ast => kind

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

Equations

• g.ast = match g with | Syntax.AstItems.Group.mk span kind ast => ast

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

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

Equations

• cls.kind = match cls with | Syntax.AstItems.ClassSetBinaryOp.mk span kind lhs rhs => kind

instance Syntax.AstItems.instToStringSetFlags : ToString Syntax.AstItems.SetFlags

Equations

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

@[irreducible]

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

Equations

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

@[irreducible]

def Syntax.AstItems.ClassSetItem.toStringClassSetItem (r : Syntax.AstItems.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 Syntax.AstItems.ClassSetUnion

Equations

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

instance Syntax.AstItems.instToStringClassSetItem : ToString Syntax.AstItems.ClassSetItem

Equations

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

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

Equations

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

def Syntax.AstItems.ClassSet.toString (r : Syntax.AstItems.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 Syntax.AstItems.ClassSet

Equations

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

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

Equations

• rep.op = match rep with | Syntax.AstItems.Repetition.mk span op greedy possessive ast => op

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

Equations

• rep.greedy = match rep with | Syntax.AstItems.Repetition.mk span op greedy possessive ast => greedy

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

Equations

• rep.possessive = match rep with | Syntax.AstItems.Repetition.mk span op greedy possessive ast => possessive

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

Equations

• rep.ast = match rep with | Syntax.AstItems.Repetition.mk span op greedy possessive ast => ast

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

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

Equations

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

@[irreducible]

def Syntax.AstItems.toString (ast : Syntax.AstItems.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 Syntax.AstItems.Ast

Equations

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

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

@[irreducible]

def Syntax.AstItems.get_fixed_width (pattern : String) (ast : Syntax.AstItems.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.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 : Syntax.AstItems.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 : Syntax.AstItems.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.