def NFA.addSink {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) : NFA A

Equations

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

def NFA.flipFinals {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) : NFA A

Equations

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

def product {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (final? : Bool → Bool → Bool) (m1 : NFA A) (m2 : NFA A) : NFA A

Equations

• product final? m1 m2 = product.go final? m1 m2 (product.init m1 m2 { m := NFA.empty, map := ∅, worklist := ∅ })

def product.init {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m1 : NFA A) (m2 : NFA A) (st : product.State) : product.State

Equations

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

@[irreducible]

def product.go {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (final? : Bool → Bool → Bool) (m1 : NFA A) (m2 : NFA A) (st0 : product.State) : NFA A

Equations

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

def NFA.inter {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m1 : NFA A) (m2 : NFA A) : NFA A

Equations

• m1.inter m2 = product (fun (b1 b2 : Bool) => b1 && b2) m1 m2

def NFA.union {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m1 : NFA A) (m2 : NFA A) : NFA A

Equations

• m1.union m2 = product (fun (b1 b2 : Bool) => b1 || b2) m1.addSink m2.addSink

def HashSet.inter {A : Type u_1} [BEq A] [Hashable A] (m1 : Std.HashSet A) (m2 : Std.HashSet A) : Std.HashSet A

Equations

• HashSet.inter m1 m2 = Std.HashSet.fold (fun (mi : Std.HashSet A) (x : A) => if m2.contains x = true then mi.insert x else mi) Std.HashSet.empty m1

def Std.HashSet.isDisjoint {A : Type u_1} [BEq A] [Hashable A] (m1 : Std.HashSet A) (m2 : Std.HashSet A) : Bool

Equations

• m1.isDisjoint m2 = (HashSet.inter m1 m2).isEmpty

def HashSet.areIncluded {A : Type u_1} [BEq A] [Hashable A] (m1 : Std.HashSet A) (m2 : Std.HashSet A) : Bool

Equations

• HashSet.areIncluded m1 m2 = m1.all fun (x : A) => m2.contains x

instance hashableHashSet {A : Type} [BEq A] [Hashable A] : Hashable (Std.HashSet A)

Equations

• hashableHashSet = { hash := fun (s : Std.HashSet A) => Std.HashSet.fold (fun (h : UInt64) (x : A) => mixHash h (hash x)) 0 s }

def NFA.determinize {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (mi : NFA A) : NFA A

Equations

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

@[irreducible]

def NFA.determinize.go {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (mi : NFA A) (st : NFA.determinize.St) : NFA A

Equations

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

def NFA.neg {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) : NFA A

Equations

• m.neg = m.determinize.flipFinals

def NFA.isIncluded {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m1 : NFA A) (m2 : NFA A) : Bool

Returns true when L(m1) ⊆ L(m2)

Equations

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

@[irreducible]

def NFA.isIncluded.go {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m1 : NFA A) (m2 : NFA A) (st : isIncluded.State) : Bool

Equations

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

def NFA.isUniversal {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) : Bool

Returns true when L(m) = A*

Equations

• m.isUniversal = NFA.isUniversal.go m { visited := ∅, worklist := Array.singleton m.initials }

@[irreducible]

def NFA.isUniversal.go {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) (st : isUniversal.State) : Bool

Equations

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

def NFA.emptyWord {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] : NFA A

Recognizes the empty word

Equations

• NFA.emptyWord = match NFA.empty.newState with | (s, m) => let m := m.addInitial s; let m := m.addFinal s; m

def NFA.isUniversal' {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) : Bool

Returns true when L(m) ∪ {ε} = A*. This is useful because the bitvector of with width zero has strange properties.

Equations

• m.isUniversal' = (m.union NFA.emptyWord).isUniversal

def NFA.isEmpty {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) : Bool

Equations

• m.isEmpty = m.finals.isEmpty

def NFA.isNotEmpty {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) : Bool

Equations

• m.isNotEmpty = !m.finals.isEmpty

instance instHashableBitVec_sSA {n : ℕ} : Hashable (BitVec n)

Equations

• instHashableBitVec_sSA = { hash := fun (x : BitVec n) => hash x.toFin }

def transport {n2 : ℕ} {n1 : ℕ} (f : Fin n2 → Fin n1) (bv : BitVec n1) : BitVec n2

Equations

• transport f bv = List.foldl (fun (bv' : BitVec n2) (i : Fin n2) => bv' ||| BitVec.twoPow n2 ↑i * ↑bv[f i].toNat) (BitVec.zero n2) (Fin.list n2)

def NFA.lift {n1 : ℕ} {n2 : ℕ} (m1 : NFA (BitVec n1)) (f : Fin n1 → Fin n2) : NFA (BitVec n2)

Equations

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

def NFA.proj {n1 : ℕ} {n2 : ℕ} (m1 : NFA (BitVec n1)) (f : Fin n2 → Fin n1) : NFA (BitVec n2)

Equations

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