instance Auto.instBEqSumUnit_auto (σ : Type) [BEq σ] : BEq (Unit ⊕ σ)

Equations

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

instance Auto.instHashableSumUnit_auto (σ : Type) [Hashable σ] : Hashable (Unit ⊕ σ)

Equations

• Auto.instHashableSumUnit_auto σ = { hash := fun (x : Unit ⊕ σ) => match x with | Sum.inl val => hash (0, 0) | Sum.inr a => hash (1, hash a) }

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

The state of a n : NFA is a natual number The number of states is n.tr.size The set of all possible states is {0,1,...,n.tr.size}, where 0 is the initial state and n.size is the accept state n.tr represents the transition function of the NFA, where Unit is the ε transition. We assume that the accept state does not have any outward transitions, so it's not recorded in n. So, by definition, the accept state has no outcoming edges. However, the initial state might have incoming edges

• tr : Array (Std.HashMap (Unit ⊕ σ) (Array Nat))
• attrs : Array (Std.HashSet String)

instance Auto.instInhabitedNFA {a✝ : Type} {a✝¹ : BEq a✝} {a✝² : Hashable a✝} : Inhabited (NFA a✝)

Equations

• Auto.instInhabitedNFA = { default := Auto.instInhabitedNFA.default }

def Auto.instInhabitedNFA.default {a✝ : Type} {a✝¹ : BEq a✝} {a✝² : Hashable a✝} : NFA a✝

Equations

• Auto.instInhabitedNFA.default = { tr := default, attrs := default }

def Auto.NFA.toString {σ : Type} [BEq σ] [Hashable σ] [ToString σ] (n : NFA σ) : String

Equations

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

instance Auto.instToStringNFA {σ : Type} [BEq σ] [Hashable σ] [ToString σ] : ToString (NFA σ)

Equations

• Auto.instToStringNFA = { toString := Auto.NFA.toString }

def Auto.NFA.εClosureOfStates {σ : Type} [BEq σ] [Hashable σ] [ToString σ] (r : NFA σ) (ss : Std.HashSet Nat) : Std.HashSet Nat

Equations

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

def Auto.NFA.move {σ : Type} [BEq σ] [Hashable σ] [ToString σ] (r : NFA σ) (ss : Std.HashSet Nat) (c : σ) : Std.HashSet Nat

Equations

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

def Auto.NFA.moves {σ : Type} [BEq σ] [Hashable σ] [ToString σ] (r : NFA σ) (ss : Std.HashSet Nat) : Std.HashMap σ (Std.HashSet Nat)

Equations

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

def Auto.NFA.moveε {σ : Type} [BEq σ] [Hashable σ] [ToString σ] (r : NFA σ) (ss : Std.HashSet Nat) (c : σ) : Std.HashSet Nat

Equations

• r.moveε ss c = r.εClosureOfStates (r.move ss c)

def Auto.NFA.moveεMany {σ : Type} [BEq σ] [Hashable σ] [ToString σ] (r : NFA σ) (ss : Std.HashSet Nat) (cs : Array σ) : Std.HashSet Nat

Equations

• r.moveεMany ss cs = Array.foldl (fun (ss' : Std.HashSet Nat) (c : σ) => r.moveε ss' c) ss cs

def Auto.NFA.run {σ : Type} [BEq σ] [Hashable σ] [ToString σ] (r : NFA σ) (cs : Array σ) : Std.HashSet Nat

Equations

• r.run cs = r.moveεMany (r.εClosureOfStates (Std.HashSet.emptyWithCapacity.insert 0)) cs

def Auto.NFA.wf {σ : Type} [BEq σ] [Hashable σ] (n : NFA σ) : Bool

Criterion : The destination of all transitions should be ≤ n.size

Equations

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

def Auto.NFA.normalize {σ : Type} [BEq σ] [Hashable σ] (n : NFA σ) : NFA σ

Delete invalid transitions and turn the NFA into a well-formed one

Equations

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

def Auto.NFA.hasEdgeToInit {σ : Type} [BEq σ] [Hashable σ] (n : NFA σ) : Bool

Whether the NFA's initial state has incoming edges

Equations

• n.hasEdgeToInit = n.tr.any fun (hmap : Std.HashMap (Unit ⊕ σ) (Array Nat)) => hmap.toList.any fun (x : (Unit ⊕ σ) × Array Nat) => match x with | (fst, arr) => arr.contains 0

def Auto.NFA.addAttrToState {σ : Type} [BEq σ] [Hashable σ] (n : NFA σ) (s : Nat) (attr : String) : NFA σ

Add attribute to a specific state

Equations

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

def Auto.NFA.addAttr {σ : Type} [BEq σ] [Hashable σ] (n : NFA σ) (attr : String) : NFA σ

Add attribute to accept state

Equations

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

def Auto.NFA.zero {σ : Type} [BEq σ] [Hashable σ] : NFA σ

Does not accept any string

Equations

• Auto.NFA.zero = { tr := #[Std.HashMap.emptyWithCapacity], attrs := #[Std.HashSet.emptyWithCapacity, Std.HashSet.emptyWithCapacity] }

def Auto.NFA.epsilon {σ : Type} [BEq σ] [Hashable σ] : NFA σ

Only accepts empty string

Equations

• Auto.NFA.epsilon = { tr := #[Std.HashMap.emptyWithCapacity.insert (Sum.inl ()) #[1]], attrs := #[Std.HashSet.emptyWithCapacity, Std.HashSet.emptyWithCapacity] }

def Auto.NFA.ofSymb {σ : Type} [BEq σ] [Hashable σ] (c : σ) : NFA σ

Accepts a character

Equations

• Auto.NFA.ofSymb c = { tr := #[Std.HashMap.emptyWithCapacity.insert (Sum.inr c) #[1]], attrs := #[Std.HashSet.emptyWithCapacity, Std.HashSet.emptyWithCapacity] }

def Auto.NFA.plus {σ : Type} [BEq σ] [Hashable σ] (m n : NFA σ) : NFA σ

Produce an NFA whose language is the union of m's and n's

Equations

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

def Auto.NFA.multiPlus {σ : Type} [BEq σ] [Hashable σ] (as : Array (NFA σ)) : NFA σ

Equations

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

def Auto.NFA.comp {σ : Type} [BEq σ] [Hashable σ] (m n : NFA σ) : NFA σ

Equations

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

def Auto.NFA.star {σ : Type} [BEq σ] [Hashable σ] (m : NFA σ) : NFA σ

Equations

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

def Auto.NFA.multiComp {σ : Type} [BEq σ] [Hashable σ] (a : Array (NFA σ)) : NFA σ

Equations

• Auto.NFA.multiComp a = Auto.NFA.multiCompAux✝ a.toList

def Auto.NFA.repeatN {σ : Type} [BEq σ] [Hashable σ] (r : NFA σ) (n : Nat) : NFA σ

Equations

• r.repeatN n = Auto.NFA.multiComp { toList := List.map (fun (x : Nat) => r) (List.range n) }

def Auto.NFA.repeatAtLeast {σ : Type} [BEq σ] [Hashable σ] (r : NFA σ) (n : Nat) : NFA σ

Equations

• r.repeatAtLeast n = (r.repeatN n).comp r.star

def Auto.NFA.repeatAtMost {σ : Type} [BEq σ] [Hashable σ] (r : NFA σ) (n : Nat) : NFA σ

Equations

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

def Auto.NFA.repeatBounded {σ : Type} [BEq σ] [Hashable σ] (r : NFA σ) (n m : Nat) : NFA σ

Equations

• r.repeatBounded n m = if n > m then Auto.NFA.epsilon else (r.repeatN n).comp (r.repeatAtMost (m - n))

def Auto.NFA.ofSymbPlus {σ : Type} [BEq σ] [Hashable σ] (cs : Array σ) : NFA σ

Accepts all characters in an array of characters

Equations

• Auto.NFA.ofSymbPlus cs = { tr := #[Std.HashMap.ofList (Array.map (fun (c : σ) => (Sum.inr c, #[1])) cs).toList], attrs := #[Std.HashSet.emptyWithCapacity, Std.HashSet.emptyWithCapacity] }

def Auto.NFA.ofSymbComp {σ : Type} [BEq σ] [Hashable σ] (s : Array σ) : NFA σ

An NFA UInt32 that accepts exactly a string

Equations

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

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

• accepts : Std.HashSet Nat
• tr : Array (Std.HashMap σ Nat)
• attrs : Array (Std.HashSet String)

instance Auto.instInhabitedDFA {a✝ : Type} {a✝¹ : BEq a✝} {a✝² : Hashable a✝} : Inhabited (DFA a✝)

Equations

• Auto.instInhabitedDFA = { default := Auto.instInhabitedDFA.default }

def Auto.instInhabitedDFA.default {a✝ : Type} {a✝¹ : BEq a✝} {a✝² : Hashable a✝} : DFA a✝

Equations

• Auto.instInhabitedDFA.default = { accepts := default, tr := default, attrs := default }

def Auto.DFA.toString {σ : Type} [BEq σ] [Hashable σ] [ToString σ] (d : DFA σ) : String

Equations

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

instance Auto.instToStringDFA {σ : Type} [BEq σ] [Hashable σ] [ToString σ] : ToString (DFA σ)

Equations

• Auto.instToStringDFA = { toString := Auto.DFA.toString }

def Auto.DFA.move {σ : Type} [BEq σ] [Hashable σ] [ToString σ] (d : DFA σ) (s : Nat) (c : σ) : Nat

Equations

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

def Auto.DFA.ofNFA {σ : Type} [BEq σ] [Hashable σ] [ToString σ] (n : NFA σ) : DFA σ

Equations

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