inductive Auto.Regex.CC.Ty : Type

• all : Ty
• upper : Ty
• lower : Ty
• alpha : Ty
• digit : Ty
• alnum : Ty
• xdigit : Ty
• punct : Ty
• blank : Ty
• space : Ty
• cntrl : Ty
• graph : Ty
• print : Ty

instance Auto.Regex.CC.instBEqTy : BEq Ty

Equations

• Auto.Regex.CC.instBEqTy = { beq := Auto.Regex.CC.instBEqTy.beq }

def Auto.Regex.CC.instBEqTy.beq : Ty → Ty → Bool

Equations

• Auto.Regex.CC.instBEqTy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Auto.Regex.CC.instHashableTy : Hashable Ty

Equations

• Auto.Regex.CC.instHashableTy = { hash := Auto.Regex.CC.instHashableTy.hash }

def Auto.Regex.CC.instHashableTy.hash : Ty → UInt64

Equations

• Auto.Regex.CC.instHashableTy.hash Auto.Regex.CC.Ty.all = 0
• Auto.Regex.CC.instHashableTy.hash Auto.Regex.CC.Ty.upper = 1
• Auto.Regex.CC.instHashableTy.hash Auto.Regex.CC.Ty.lower = 2
• Auto.Regex.CC.instHashableTy.hash Auto.Regex.CC.Ty.alpha = 3
• Auto.Regex.CC.instHashableTy.hash Auto.Regex.CC.Ty.digit = 4
• Auto.Regex.CC.instHashableTy.hash Auto.Regex.CC.Ty.alnum = 5
• Auto.Regex.CC.instHashableTy.hash Auto.Regex.CC.Ty.xdigit = 6
• Auto.Regex.CC.instHashableTy.hash Auto.Regex.CC.Ty.punct = 7
• Auto.Regex.CC.instHashableTy.hash Auto.Regex.CC.Ty.blank = 8
• Auto.Regex.CC.instHashableTy.hash Auto.Regex.CC.Ty.space = 9
• Auto.Regex.CC.instHashableTy.hash Auto.Regex.CC.Ty.cntrl = 10
• Auto.Regex.CC.instHashableTy.hash Auto.Regex.CC.Ty.graph = 11
• Auto.Regex.CC.instHashableTy.hash Auto.Regex.CC.Ty.print = 12

instance Auto.Regex.CC.instInhabitedTy : Inhabited Ty

Equations

• Auto.Regex.CC.instInhabitedTy = { default := Auto.Regex.CC.instInhabitedTy.default }

def Auto.Regex.CC.instInhabitedTy.default : Ty

Equations

• Auto.Regex.CC.instInhabitedTy.default = Auto.Regex.CC.Ty.all

def Auto.Regex.CC.Ty.toString : Ty → String

Equations

• Auto.Regex.CC.Ty.all.toString = Auto.Regex.CC.alls✝
• Auto.Regex.CC.Ty.upper.toString = Auto.Regex.CC.uppers✝
• Auto.Regex.CC.Ty.lower.toString = Auto.Regex.CC.lowers✝
• Auto.Regex.CC.Ty.alpha.toString = Auto.Regex.CC.alphas✝
• Auto.Regex.CC.Ty.digit.toString = Auto.Regex.CC.digits✝
• Auto.Regex.CC.Ty.alnum.toString = Auto.Regex.CC.alnums✝
• Auto.Regex.CC.Ty.xdigit.toString = Auto.Regex.CC.xdigits✝
• Auto.Regex.CC.Ty.punct.toString = Auto.Regex.CC.puncts✝
• Auto.Regex.CC.Ty.blank.toString = Auto.Regex.CC.blanks✝
• Auto.Regex.CC.Ty.space.toString = Auto.Regex.CC.spaces✝
• Auto.Regex.CC.Ty.cntrl.toString = Auto.Regex.CC.cntrls✝
• Auto.Regex.CC.Ty.graph.toString = Auto.Regex.CC.graphs✝
• Auto.Regex.CC.Ty.print.toString = Auto.Regex.CC.prints✝

instance Auto.Regex.CC.instToStringTy : ToString Ty

Equations

• Auto.Regex.CC.instToStringTy = { toString := Auto.Regex.CC.Ty.toString }

def Auto.Regex.instHashableChar_auto : Hashable Char

Equations

• Auto.Regex.instHashableChar_auto = { hash := fun (c : Char) => hash c.val }

inductive Auto.Regex.EREBracket : Type

• cc : CC.Ty → EREBracket
• inStr : String → EREBracket
• plus : Array EREBracket → EREBracket
• minus (b1 b2 : EREBracket) : EREBracket

instance Auto.Regex.instBEqEREBracket : BEq EREBracket

Equations

• Auto.Regex.instBEqEREBracket = { beq := Auto.Regex.instBEqEREBracket.beq }

partial def Auto.Regex.instBEqEREBracket.beq : EREBracket → EREBracket → Bool

partial def Auto.Regex.instHashableEREBracket.hash : EREBracket → UInt64

instance Auto.Regex.instHashableEREBracket : Hashable EREBracket

Equations

• Auto.Regex.instHashableEREBracket = { hash := Auto.Regex.instHashableEREBracket.hash }

instance Auto.Regex.instInhabitedEREBracket : Inhabited EREBracket

Equations

• Auto.Regex.instInhabitedEREBracket = { default := Auto.Regex.instInhabitedEREBracket.default }

def Auto.Regex.instInhabitedEREBracket.default : EREBracket

Equations

• Auto.Regex.instInhabitedEREBracket.default = Auto.Regex.EREBracket.cc default

def Auto.Regex.EREBracket.neg (b : EREBracket) : EREBracket

Taking complement of b with respect to the set of ascii characters

Equations

• b.neg = b.minus (Auto.Regex.EREBracket.cc Auto.Regex.CC.Ty.all)

partial def Auto.Regex.EREBracket.toHashSet : EREBracket → Std.HashSet Char

partial def Auto.Regex.EREBracket.toHashSet.go : List EREBracket → Std.HashSet Char

def Auto.Regex.EREBracket.toString (e : EREBracket) : String

Equations

• e.toString = { data := e.toHashSet.toList }

instance Auto.Regex.instToStringEREBracket : ToString EREBracket

Equations

• Auto.Regex.instToStringEREBracket = { toString := Auto.Regex.EREBracket.toString }

inductive Auto.Regex.ERE : Type

• bracket : EREBracket → ERE
• bracketN : EREBracket → ERE
• startp : ERE
• endp : ERE
• epsilon : ERE
• star : ERE → ERE
• repN : ERE → (n : Nat) → ERE
• repGe : ERE → (n : Nat) → ERE
• repLe : ERE → (n : Nat) → ERE
• repGeLe : ERE → (n m : Nat) → ERE
• comp : Array ERE → ERE
• plus : Array ERE → ERE
• attr : ERE → String → ERE

instance Auto.Regex.instBEqERE : BEq ERE

Equations

• Auto.Regex.instBEqERE = { beq := Auto.Regex.instBEqERE.beq }

partial def Auto.Regex.instBEqERE.beq : ERE → ERE → Bool

partial def Auto.Regex.instHashableERE.hash : ERE → UInt64

instance Auto.Regex.instHashableERE : Hashable ERE

Equations

• Auto.Regex.instHashableERE = { hash := Auto.Regex.instHashableERE.hash }

def Auto.Regex.instInhabitedERE.default : ERE

Equations

• Auto.Regex.instInhabitedERE.default = Auto.Regex.ERE.bracket default

instance Auto.Regex.instInhabitedERE : Inhabited ERE

Equations

• Auto.Regex.instInhabitedERE = { default := Auto.Regex.instInhabitedERE.default }

def Auto.Regex.ERE.inStr (s : String) : ERE

Match any character in the string

Equations

• Auto.Regex.ERE.inStr s = Auto.Regex.ERE.bracket (Auto.Regex.EREBracket.inStr s)

def Auto.Regex.ERE.ofStr (s : String) : ERE

Match the given string

Equations

• Auto.Regex.ERE.ofStr s = Auto.Regex.ERE.comp { toList := List.map (fun (c : Char) => Auto.Regex.ERE.inStr { data := [c] }) s.toList }

def Auto.Regex.ERE.ofCC (c : CC.Ty) : ERE

Equations

• Auto.Regex.ERE.ofCC c = Auto.Regex.ERE.bracket (Auto.Regex.EREBracket.cc c)

def Auto.Regex.ERE.opt (e : ERE) : ERE

Optional, corresponding to ?

Equations

• e.opt = e.repLe 1

def Auto.Regex.ERE.some (e : ERE) : ERE

Nonempty sequence of, corresponding to +

Equations

• e.some = e.repGe 1

partial def Auto.Regex.ERE.brackets : ERE → Array EREBracket

partial def Auto.Regex.ERE.normalizeBrackets : ERE → ERE

structure Auto.Regex.CharGrouping (σ : Type) [Hashable σ] [BEq σ] : Type

Given an ERE, group characters that behaves the same, according to all the brackets in this ERE

• ngroup : Nat
• all : Std.HashSet σ
• charMap : Std.HashMap σ Nat

def Auto.Regex.instInhabitedCharGrouping.default {a✝ : Type} {a✝¹ : Hashable a✝} {a✝² : BEq a✝} : CharGrouping a✝

Equations

• Auto.Regex.instInhabitedCharGrouping.default = { ngroup := default, all := default, charMap := default }

instance Auto.Regex.instInhabitedCharGrouping {a✝ : Type} {a✝¹ : Hashable a✝} {a✝² : BEq a✝} : Inhabited (CharGrouping a✝)

Equations

• Auto.Regex.instInhabitedCharGrouping = { default := Auto.Regex.instInhabitedCharGrouping.default }

structure Auto.Regex.ADFA (σ : Type) [Hashable σ] [BEq σ] : Type

Annotated DFA, the lexer table

• dfa : DFA Nat
• cg : CharGrouping σ

instance Auto.Regex.instInhabitedADFA {a✝ : Type} {a✝¹ : Hashable a✝} {a✝² : BEq a✝} : Inhabited (ADFA a✝)

Equations

• Auto.Regex.instInhabitedADFA = { default := Auto.Regex.instInhabitedADFA.default }

def Auto.Regex.instInhabitedADFA.default {a✝ : Type} {a✝¹ : Hashable a✝} {a✝² : BEq a✝} : ADFA a✝

Equations

• Auto.Regex.instInhabitedADFA.default = { dfa := default, cg := default }

def Auto.Regex.CharGrouping.wf {σ : Type} [Hashable σ] [BEq σ] : CharGrouping σ → Bool

Equations

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

def Auto.Regex.CharGrouping.groups {σ : Type} [Hashable σ] [BEq σ] : CharGrouping σ → Array (Std.HashSet σ)

Equations

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

def Auto.Regex.CharGrouping.toStringAux {σ : Type} [Hashable σ] [BEq σ] : CharGrouping σ → (symbListToString : Array σ → String) → String

Equations

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

def Auto.Regex.CharGrouping.toString {σ : Type} [Hashable σ] [BEq σ] [ToString σ] (cg : CharGrouping σ) : String

Equations

• cg.toString = cg.toStringAux toString

instance Auto.Regex.instToStringCharGrouping {σ : Type} [Hashable σ] [BEq σ] [ToString σ] : ToString (CharGrouping σ)

Equations

• Auto.Regex.instToStringCharGrouping = { toString := Auto.Regex.CharGrouping.toString }

def Auto.Regex.CharGrouping.getGroup {σ : Type} [Hashable σ] [BEq σ] (cg : CharGrouping σ) (c : σ) : Nat

Equations

• cg.getGroup c = match cg.charMap.get? c with | some g => g | none => cg.ngroup + 2

def Auto.Regex.ADFA.toStringAux {σ : Type} [Hashable σ] [BEq σ] : ADFA σ → (symbListToString : Array σ → String) → String

Equations

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

def Auto.Regex.ADFA.toString {σ : Type} [Hashable σ] [BEq σ] [ToString σ] (a : ADFA σ) : String

Equations

• a.toString = a.toStringAux fun (l : Array σ) => toString l.toList

instance Auto.Regex.instToStringADFA {σ : Type} [Hashable σ] [BEq σ] [ToString σ] : ToString (ADFA σ)

Equations

• Auto.Regex.instToStringADFA = { toString := Auto.Regex.ADFA.toString }

def Auto.Regex.ADFA.getAttrs {σ : Type} [Hashable σ] [BEq σ] [ToString σ] (a : ADFA σ) (state : Nat) : Std.HashSet String

Equations

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

def Auto.Regex.CharGrouping.toStringForChar (cg : CharGrouping Char) : String

Equations

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

instance Auto.Regex.instToStringCharGroupingChar : ToString (CharGrouping Char)

Equations

• Auto.Regex.instToStringCharGroupingChar = { toString := Auto.Regex.CharGrouping.toStringForChar }

def Auto.Regex.ADFA.toStringForChar (a : ADFA Char) : String

Equations

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

instance Auto.Regex.instToStringADFAChar : ToString (ADFA Char)

Equations

• Auto.Regex.instToStringADFAChar = { toString := Auto.Regex.ADFA.toStringForChar }

def Auto.Regex.ERE.charGrouping (e : ERE) : CharGrouping Char

Equations

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

def Auto.Regex.ERE.toADFA (e : ERE) (prependStartP : Bool := true) : ADFA Char

Equations

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

structure Auto.Regex.LexConfig : Type

• short : Bool
• strict : Bool
• initS : Nat
• prependBeginS : Bool
• appendEndS : Bool

inductive Auto.Regex.LexResultTy : Type

• complete : LexResultTy
• incomplete : LexResultTy
• malformed : LexResultTy

def Auto.Regex.instInhabitedLexResultTy.default : LexResultTy

Equations

• Auto.Regex.instInhabitedLexResultTy.default = Auto.Regex.LexResultTy.complete

instance Auto.Regex.instInhabitedLexResultTy : Inhabited LexResultTy

Equations

• Auto.Regex.instInhabitedLexResultTy = { default := Auto.Regex.instInhabitedLexResultTy.default }

instance Auto.Regex.instHashableLexResultTy : Hashable LexResultTy

Equations

• Auto.Regex.instHashableLexResultTy = { hash := Auto.Regex.instHashableLexResultTy.hash }

def Auto.Regex.instHashableLexResultTy.hash : LexResultTy → UInt64

Equations

• Auto.Regex.instHashableLexResultTy.hash Auto.Regex.LexResultTy.complete = 0
• Auto.Regex.instHashableLexResultTy.hash Auto.Regex.LexResultTy.incomplete = 1
• Auto.Regex.instHashableLexResultTy.hash Auto.Regex.LexResultTy.malformed = 2

instance Auto.Regex.instBEqLexResultTy : BEq LexResultTy

Equations

• Auto.Regex.instBEqLexResultTy = { beq := Auto.Regex.instBEqLexResultTy.beq }

def Auto.Regex.instBEqLexResultTy.beq : LexResultTy → LexResultTy → Bool

Equations

• Auto.Regex.instBEqLexResultTy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Auto.Regex.LexResultTy.toString : LexResultTy → String

Equations

• Auto.Regex.LexResultTy.complete.toString = "LexResultTy.complete"
• Auto.Regex.LexResultTy.incomplete.toString = "LexResultTy.incomplete"
• Auto.Regex.LexResultTy.malformed.toString = "LexResultTy.malformed"

instance Auto.Regex.instToStringLexResultTy : ToString LexResultTy

Equations

• Auto.Regex.instToStringLexResultTy = { toString := Auto.Regex.LexResultTy.toString }

structure Auto.Regex.LexResult : Type

• type : LexResultTy
• matched : Substring
• endSMatched : Bool
• state : Nat

def Auto.Regex.instInhabitedLexResult.default : LexResult

Equations

• Auto.Regex.instInhabitedLexResult.default = { type := default, matched := default, endSMatched := default, state := default }

instance Auto.Regex.instInhabitedLexResult : Inhabited LexResult

Equations

• Auto.Regex.instInhabitedLexResult = { default := Auto.Regex.instInhabitedLexResult.default }

instance Auto.Regex.instBEqLexResult : BEq LexResult

Equations

• Auto.Regex.instBEqLexResult = { beq := Auto.Regex.instBEqLexResult.beq }

def Auto.Regex.instBEqLexResult.beq : LexResult → LexResult → Bool

Equations

• One or more equations did not get rendered due to their size.
• Auto.Regex.instBEqLexResult.beq x✝¹ x✝ = false

def Auto.Regex.LexResult.toString : LexResult → String

Equations

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

instance Auto.Regex.instToStringLexResult : ToString LexResult

Equations

• Auto.Regex.instToStringLexResult = { toString := Auto.Regex.LexResult.toString }

def Auto.Regex.ERE.ADFALexEagerL (a : ADFA Char) (s : Substring) (cfg : LexConfig) : LexResult

Usage : First use ERE.toADFA to generate the lexing table in another file <f> and use initialize to store it, then call the following function in another file, where the ADFA is the one initialized in <f>. Leftmost match, eager (in finding the first matching character) and matches at least one character. short = false : Longest match, default short = true : Shortest match strict = false: Start from the first valid character, default strict = true : Start from the first character of s Note that if we can't find the matching first character with strict = false, we just return incomplete This function takes an ADFA generated by ERE.toADFA (e : ERE), a string s. It first finds the leftmost character in s that is a [valid first character of the lexicon] (thus the name eager). Then, it returns the longest match (as a substring) if there is one, and returns none otherwise. We prepend s with the "beginning of string" group and append to s the "end of string" group

Equations

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