High-level intermediate representation for a regular expression.

A high-level intermediate representation Syntax.Hir for a regular expression.

@[reducible, inline]

abbrev Syntax.ClassUnicodeRange : Type

Equations

• Syntax.ClassUnicodeRange = NonemptyInterval Char

instance Syntax.instInhabitedClassUnicodeRange : Inhabited Syntax.ClassUnicodeRange

Equations

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

structure Syntax.ClassUnicode : Type

• set : IntervalSet Char

instance Syntax.instToStringNonemptyIntervalChar : ToString (NonemptyInterval Char)

Equations

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

instance Syntax.instToStringIntervalSetChar : ToString (IntervalSet Char)

Equations

• Syntax.instToStringIntervalSetChar = { toString := fun (set : IntervalSet Char) => toString "ranges: " ++ toString set.intervals ++ toString "" }

instance Syntax.instToStringClassUnicode : ToString Syntax.ClassUnicode

Equations

• Syntax.instToStringClassUnicode = { toString := fun (cls : Syntax.ClassUnicode) => toString "" ++ toString cls.set ++ toString "" }

instance Syntax.instInhabitedClassUnicode : Inhabited Syntax.ClassUnicode

see UInt32.isValidChar

Equations

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

def Syntax.ClassUnicode.empty : Syntax.ClassUnicode

Equations

• Syntax.ClassUnicode.empty = { set := { intervals := #[], isNonOverlapping := ⋯ } }

def Syntax.ClassUnicode.canonicalize (cls : Syntax.ClassUnicode) : Syntax.ClassUnicode

Equations

• cls.canonicalize = { set := IntervalSet.canonicalize cls.set.intervals }

def Syntax.ClassUnicode.union (cls1 cls2 : Syntax.ClassUnicode) : Syntax.ClassUnicode

Equations

• cls1.union cls2 = { set := cls1.set.union cls2.set }

def Syntax.ClassUnicode.intersection (cls1 cls2 : Syntax.ClassUnicode) : Syntax.ClassUnicode

Equations

• cls1.intersection cls2 = { set := cls1.set.intersection cls2.set }

def Syntax.ClassUnicode.difference (cls1 cls2 : Syntax.ClassUnicode) : Syntax.ClassUnicode

Equations

• cls1.difference cls2 = { set := cls1.set.difference cls2.set }

def Syntax.ClassUnicode.symmetric_difference (cls1 cls2 : Syntax.ClassUnicode) : Syntax.ClassUnicode

Equations

• cls1.symmetric_difference cls2 = { set := cls1.set.symmetric_difference cls2.set }

def Syntax.ClassUnicode.negate (cls : Syntax.ClassUnicode) : Syntax.ClassUnicode

Equations

• cls.negate = { set := cls.set.negate }

def Syntax.ClassUnicode.case_fold (cls : Syntax.ClassUnicode) : Syntax.ClassUnicode

Equations

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

inductive Syntax.Class : Type

• Unicode: Syntax.ClassUnicode → Syntax.Class

  A set of characters represented by Unicode scalar values.

instance Syntax.instToStringClass : ToString Syntax.Class

Equations

• Syntax.instToStringClass = { toString := fun (cls : Syntax.Class) => match cls with | Syntax.Class.Unicode cls => toString "" ++ toString cls ++ toString "" }

inductive Syntax.Look : Type

The high-level intermediate representation for a look-around assertion.

• Start: Syntax.Look

  Match the beginning of text.

• End: Syntax.Look

  Match the end of text.

• EndWithOptionalLF: Syntax.Look

  Match the end of text (before optional newline).

• StartLF: Syntax.Look

  Match the beginning of a line or the beginning of text.

• EndLF: Syntax.Look

  Match the end of a line or the end of text.

• StartCRLF: Syntax.Look

  Match the beginning of a line or the beginning of text.

• EndCRLF: Syntax.Look

  Match the end of a line or the end of text.

• WordUnicode: Syntax.Look

  Match a Unicode-aware word boundary.

• WordUnicodeNegate: Syntax.Look

  Match a Unicode-aware negation of a word boundary.

• WordStartUnicode: Syntax.Look

  Match the start of a Unicode word boundary.

• WordEndUnicode: Syntax.Look

  Match the end of a Unicode word boundary.

• WordStartHalfUnicode: Syntax.Look

  Match the start half of a Unicode word boundary.

• WordEndHalfUnicode: Syntax.Look

  Match the end half of a Unicode word boundary.

• PreviousMatch: Syntax.Look

  Match the end of the previous match or start of string.

• ClearMatches: Syntax.Look

  Clear all matches.

instance Syntax.instBEqLook : BEq Syntax.Look

Equations

• Syntax.instBEqLook = { beq := Syntax.beqLook✝ }

def Syntax.Look.toString : Syntax.Look → String

Equations

• Syntax.Look.Start.toString = toString "Start"
• Syntax.Look.End.toString = toString "End"
• Syntax.Look.EndWithOptionalLF.toString = toString "EndWithOptionalLF"
• Syntax.Look.StartLF.toString = toString "StartLF"
• Syntax.Look.EndLF.toString = toString "EndLF"
• Syntax.Look.StartCRLF.toString = toString "StartCRLF"
• Syntax.Look.EndCRLF.toString = toString "EndCRLF"
• Syntax.Look.WordUnicode.toString = toString "WordUnicode"
• Syntax.Look.WordUnicodeNegate.toString = toString "WordUnicodeNegate"
• Syntax.Look.WordStartUnicode.toString = toString "WordStartUnicode"
• Syntax.Look.WordEndUnicode.toString = toString "WordEndUnicode"
• Syntax.Look.WordStartHalfUnicode.toString = toString "WordStartHalfUnicode"
• Syntax.Look.WordEndHalfUnicode.toString = toString "WordEndHalfUnicode"
• Syntax.Look.PreviousMatch.toString = toString "PreviousMatch"
• Syntax.Look.ClearMatches.toString = toString "ClearMatches"

instance Syntax.instToStringLook : ToString Syntax.Look

Equations

• Syntax.instToStringLook = { toString := Syntax.Look.toString }

structure Syntax.Properties : Type

A type that collects various properties of an HIR value.

• minimum_len : Option UInt32
• maximum_len : Option UInt32

instance Syntax.instInhabitedProperties : Inhabited Syntax.Properties

Equations

• Syntax.instInhabitedProperties = { default := { minimum_len := none, maximum_len := none } }

structure Syntax.Flags : Type

A translator's representation of a regular expression's flags at any given moment in time.

• case_insensitive : Option Bool
• multi_line : Option Bool
• dot_matches_new_line : Option Bool
• swap_greed : Option Bool
• crlf : Option Bool
• extended : Option Regex.Grammar.ExtendedKind

instance Syntax.instInhabitedFlags : Inhabited Syntax.Flags

Equations

• Syntax.instInhabitedFlags = { default := { case_insensitive := none, multi_line := none, dot_matches_new_line := none, swap_greed := none, crlf := none, extended := none } }

instance Syntax.instToStringFlags : ToString Syntax.Flags

Equations

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

inductive Syntax.Lookaround : Type

The high-level intermediate representation for a look-around assertion.

• PositiveLookahead: Syntax.Hir → Syntax.Lookaround
• NegativeLookahead: Syntax.Hir → Syntax.Lookaround
• PositiveLookbehind: Nat → Syntax.Hir → Syntax.Lookaround
• NegativeLookbehind: Nat → Syntax.Hir → Syntax.Lookaround

inductive Syntax.Repetition : Type

A concatenation of regular expressions.

• mk: Nat → Option Nat → Bool → Bool → Syntax.Hir → Syntax.Repetition

inductive Syntax.Capture : Type

The high-level intermediate representation for a capturing group.

• mk: Nat → Option String → Syntax.Hir → Syntax.Capture

inductive Syntax.HirKind : Type

The underlying kind of an arbitrary [Hir] expression.

• Empty: Syntax.HirKind

  The empty regular expression, which matches everything, including the empty string.

• Literal: Char → Syntax.HirKind

  A literal string that matches exactly these bytes.

• BackRef: Bool → Nat → Syntax.HirKind

  A backrefence to a capturung group.

• Class: Syntax.Class → Syntax.HirKind

  A single character class that matches any of the characters in the class.

• Look: Syntax.Look → Syntax.HirKind

  A look-around assertion. A look-around match always has zero length.

• Lookaround: Syntax.Lookaround → Syntax.HirKind

  A complex look-around assertion.

• Repetition: Syntax.Repetition → Syntax.HirKind

  A repetition operation applied to a sub-expression.

• Capture: Syntax.Capture → Syntax.HirKind

  A capturing group, which contains a sub-expression.

• Concat: Array Syntax.Hir → Syntax.HirKind

  A concatenation of expressions.

• Alternation: Array Syntax.Hir → Syntax.HirKind

  An alternation of expressions.

inductive Syntax.Hir : Type

A high-level intermediate representation (HIR) for a regular expression.

• mk: Syntax.HirKind → Syntax.Properties → Syntax.Hir

instance Syntax.instInhabitedHir : Inhabited Syntax.Hir

Equations

• Syntax.instInhabitedHir = { default := Syntax.Hir.mk Syntax.HirKind.Empty default }

def Syntax.Hir.kind (hir : Syntax.Hir) : Syntax.HirKind

Equations

• (Syntax.Hir.mk kind props).kind = kind

theorem Syntax.Hir.sizeOfKindOfHir (hir : Syntax.Hir) : sizeOf hir.kind < sizeOf hir

def Syntax.Hir.properties (hir : Syntax.Hir) : Syntax.Properties

Equations

• (Syntax.Hir.mk kind props).properties = props

def Syntax.Hir.toProperties (kind : Syntax.HirKind) : Syntax.Properties

Equations

• Syntax.Hir.toProperties (Syntax.HirKind.Class (Syntax.Class.Unicode cls)) = { minimum_len := if cls.set.intervals.size > 0 then some 1 else none, maximum_len := none }
• Syntax.Hir.toProperties kind = default

@[irreducible]

def Syntax.Hir.toString (hir : Syntax.Hir) (col : Nat) : String

Equations

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

@[irreducible]

def Syntax.Hir.fold {α : Type u_1} [Inhabited α] [ToString α] (hir : Syntax.Hir) (f : α → Syntax.Hir → α) (init : α) : α

Equations

• One or more equations did not get rendered due to their size.
• (Syntax.Hir.mk Syntax.HirKind.Empty props).fold f init = f (f init (Syntax.Hir.mk Syntax.HirKind.Empty props)) (Syntax.Hir.mk Syntax.HirKind.Empty props)
• (Syntax.Hir.mk (Syntax.HirKind.Literal a) props).fold f init = f (f init (Syntax.Hir.mk (Syntax.HirKind.Literal a) props)) (Syntax.Hir.mk (Syntax.HirKind.Literal a) props)
• (Syntax.Hir.mk (Syntax.HirKind.BackRef a a_1) props).fold f init = f (f init (Syntax.Hir.mk (Syntax.HirKind.BackRef a a_1) props)) (Syntax.Hir.mk (Syntax.HirKind.BackRef a a_1) props)
• (Syntax.Hir.mk (Syntax.HirKind.Class a) props).fold f init = f (f init (Syntax.Hir.mk (Syntax.HirKind.Class a) props)) (Syntax.Hir.mk (Syntax.HirKind.Class a) props)
• (Syntax.Hir.mk (Syntax.HirKind.Look a) props).fold f init = f (f init (Syntax.Hir.mk (Syntax.HirKind.Look a) props)) (Syntax.Hir.mk (Syntax.HirKind.Look a) props)
• (Syntax.Hir.mk (Syntax.HirKind.Capture a) props).fold f init = f (f init (Syntax.Hir.mk (Syntax.HirKind.Capture a) props)) (Syntax.Hir.mk (Syntax.HirKind.Capture a) props)

def Syntax.Hir.containsLookaround (hir : Syntax.Hir) : Bool

check if an hir contains .Lookaround

Equations

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

instance Syntax.instToStringHir : ToString Syntax.Hir

Equations

• Syntax.instToStringHir = { toString := fun (hir : Syntax.Hir) => hir.toString 0 }

inductive Syntax.Dot : Type

A type describing the different flavors of ..

• AnyChar: Syntax.Dot

  Matches the UTF-8 encoding of any Unicode scalar value. This is equivalent to (?su:.) and also \p{any}.

• AnyCharExceptLF: Syntax.Dot

  Matches the UTF-8 encoding of any Unicode scalar value except for \n. This is equivalent to (?u-s:.) and also [\p{any}--\n].

• AnyCharExceptCRLF: Syntax.Dot

  Matches the UTF-8 encoding of any Unicode scalar value except for \r and \n. This is equivalent to (?uR-s:.) and also [\p{any}--\r\n].

def Syntax.dot (dot : Syntax.Dot) : Syntax.Hir

Equations

• One or more equations did not get rendered due to their size.
• Syntax.dot Syntax.Dot.AnyChar = Syntax.Hir.mk (Syntax.HirKind.Class (Syntax.Class.Unicode default)) (Syntax.Hir.toProperties (Syntax.HirKind.Class (Syntax.Class.Unicode default)))

inductive Syntax.HirFrame : Type

An HirFrame is a single stack frame, represented explicitly, which is created for each item in the Ast that we traverse.

• Expr: Syntax.Hir → Syntax.HirFrame
• Literal: Char → Syntax.HirFrame
• BackRef: Bool → Nat → Syntax.HirFrame
• ClassUnicode: Syntax.ClassUnicode → Syntax.HirFrame
• Repetition: Syntax.HirFrame
• Group: Syntax.Flags → Syntax.HirFrame
• Concat: Syntax.HirFrame
• Alternation: Syntax.HirFrame

def Syntax.HirFrame.toString : Syntax.HirFrame → String

Equations

• (Syntax.HirFrame.Expr hir).toString = toString "Expr '" ++ toString hir ++ toString "'"
• (Syntax.HirFrame.Literal c).toString = toString "Literal " ++ toString c ++ toString ""
• (Syntax.HirFrame.BackRef f n).toString = toString "BackRef " ++ toString (if f = true then "case_insensitive" else "") ++ toString " " ++ toString n ++ toString ""
• (Syntax.HirFrame.ClassUnicode cls).toString = toString "ClassUnicode cls set size " ++ toString cls.set.intervals.size ++ toString ""
• Syntax.HirFrame.Repetition.toString = "Repetition"
• (Syntax.HirFrame.Group flags).toString = toString "Group " ++ toString flags ++ toString ""
• Syntax.HirFrame.Concat.toString = "Concat"
• Syntax.HirFrame.Alternation.toString = "Alternation"

def Syntax.HirFrame.unwrap_expr (frame : Syntax.HirFrame) : Except String Syntax.Hir

Equations

• (Syntax.HirFrame.Expr expr).unwrap_expr = Except.ok expr
• (Syntax.HirFrame.Literal c).unwrap_expr = Except.ok (Syntax.Hir.mk (Syntax.HirKind.Literal c) default)
• (Syntax.HirFrame.BackRef f n).unwrap_expr = Except.ok (Syntax.Hir.mk (Syntax.HirKind.BackRef f n) default)
• frame.unwrap_expr = Except.error "unwrap_expr, Literal or Expr expected"

def Syntax.HirFrame.unwrap_class_unicode (frame : Syntax.HirFrame) : Except String Syntax.ClassUnicode

Assert that the current stack frame is a Unicode class expression and return it.

Equations

• (Syntax.HirFrame.ClassUnicode cls).unwrap_class_unicode = Except.ok cls
• frame.unwrap_class_unicode = Except.error "unwrap_repetition, Repetition expected"

def Syntax.HirFrame.unwrap_repetition (frame : Syntax.HirFrame) : Except String Unit

Assert that the current stack frame is a repetition.

Equations

• Syntax.HirFrame.Repetition.unwrap_repetition = Except.ok ()
• frame.unwrap_repetition = Except.error "unwrap_repetition, Repetition expected"

def Syntax.HirFrame.unwrap_group (frame : Syntax.HirFrame) : Except String Syntax.Flags

Assert that the current stack frame is a group.

Equations

• (Syntax.HirFrame.Group flags).unwrap_group = Except.ok flags
• frame.unwrap_group = Except.error "unwrap_repetition, Repetition expected"

instance Syntax.instToStringHirFrame : ToString Syntax.HirFrame

Equations

• Syntax.instToStringHirFrame = { toString := Syntax.HirFrame.toString }