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 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

• Syntax.instToStringNonemptyIntervalChar = { toString := fun (r : NonemptyInterval Char) => toString r.fst.val.intAsString ++ toString "-" ++ toString r.snd.val.intAsString }

instance Syntax.instToStringIntervalSetChar : ToString (IntervalSet Char)

Equations

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

instance Syntax.instToStringClassUnicode : ToString ClassUnicode

Equations

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

instance Syntax.instInhabitedClassUnicode : Inhabited ClassUnicode

see UInt32.isValidChar

Equations

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

def Syntax.ClassUnicode.empty : ClassUnicode

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

inductive Syntax.Class : Type

• Unicode : ClassUnicode → Class

  A set of characters represented by Unicode scalar values.

instance Syntax.instToStringClass : ToString Class

Equations

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

inductive Syntax.Look : Type

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

• Start : Look

  Match the beginning of text.

• End : Look

  Match the end of text.

• EndWithOptionalLF : Look

  Match the end of text (before optional newline).

• StartLF : Look

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

• EndLF : Look

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

• StartCRLF : Look

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

• EndCRLF : Look

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

• WordUnicode : Look

  Match a Unicode-aware word boundary.

• WordUnicodeNegate : Look

  Match a Unicode-aware negation of a word boundary.

• WordStartUnicode : Look

  Match the start of a Unicode word boundary.

• WordEndUnicode : Look

  Match the end of a Unicode word boundary.

• WordStartHalfUnicode : Look

  Match the start half of a Unicode word boundary.

• WordEndHalfUnicode : Look

  Match the end half of a Unicode word boundary.

• PreviousMatch : Look

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

• ClearMatches : Look

  Clear all matches.

def Syntax.instBEqLook.beq : Look → Look → Bool

Equations

• Syntax.instBEqLook.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Syntax.instBEqLook : BEq Look

Equations

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

def Syntax.Look.toString : 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 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 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 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 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 : Hir → Lookaround
• NegativeLookahead : Hir → Lookaround
• PositiveLookbehind : Nat → Hir → Lookaround
• NegativeLookbehind : Nat → Hir → Lookaround

inductive Syntax.Repetition : Type

A concatenation of regular expressions.

• mk (min : Nat) (max : Option Nat) (greedy possessive : Bool) (sub : Hir) : Repetition

inductive Syntax.Capture : Type

The high-level intermediate representation for a capturing group.

• mk (index : Nat) (name : Option String) (sub : Hir) : Capture

inductive Syntax.HirKind : Type

The underlying kind of an arbitrary [Hir] expression.

• Empty : HirKind

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

• Literal : Char → HirKind

  A literal string that matches exactly these bytes.

• BackRef : Bool → Nat → HirKind

  A backrefence to a capturung group.

• Class : Syntax.Class → HirKind

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

• Look : Syntax.Look → HirKind

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

• Lookaround : Syntax.Lookaround → HirKind

  A complex look-around assertion.

• Repetition : Syntax.Repetition → HirKind

  A repetition operation applied to a sub-expression.

• Capture : Syntax.Capture → HirKind

  A capturing group, which contains a sub-expression.

• Concat : Array Hir → HirKind

  A concatenation of expressions.

• Alternation : Array Hir → HirKind

  An alternation of expressions.

inductive Syntax.Hir : Type

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

• mk (kind : HirKind) (props : Properties) : Hir

instance Syntax.instInhabitedHir : Inhabited Hir

Equations

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

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

Equations

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

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

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

Equations

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

def Syntax.Hir.toProperties (kind : HirKind) : 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 : 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 : Hir) (f : α → 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 : 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 Hir

Equations

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

inductive Syntax.Dot : Type

A type describing the different flavors of ..

• AnyChar : Dot

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

• AnyCharExceptLF : 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 : 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 : Dot) : 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 : Hir → HirFrame
• Literal : Char → HirFrame
• BackRef : Bool → Nat → HirFrame
• ClassUnicode : Syntax.ClassUnicode → HirFrame
• Repetition : HirFrame
• Group (old_flags : Flags) : HirFrame
• Concat : HirFrame
• Alternation : HirFrame

def Syntax.HirFrame.toString : HirFrame → String

Equations

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

def Syntax.HirFrame.unwrap_expr (frame : HirFrame) : Except String 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 : 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 : 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 : HirFrame) : Except String 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 HirFrame

Equations

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