structure Array.PrefixTable (α : Type u_1) extends Array : Type u_1

Prefix table for the Knuth-Morris-Pratt matching algorithm

This is an array of the form t = [(x₀,n₀), (x₁,n₁), (x₂, n₂), ...] where for each i, nᵢ is the length of the longest proper prefix of xs = [x₀,x₁,...,xᵢ] which is also a suffix of xs.

• toList : List (α × Nat)
• valid : ∀ {i : Nat} (h : i < self.size), self.toArray[i].snd ≤ i

  Validity condition to help with termination proofs

theorem Array.PrefixTable.valid {α : Type u_1} (self : Array.PrefixTable α) {i : Nat} (h : i < self.size) : self.toArray[i].snd ≤ i

Validity condition to help with termination proofs

instance Array.instInhabitedPrefixTable {α : Type u_1} : Inhabited (Array.PrefixTable α)

Equations

• Array.instInhabitedPrefixTable = { default := { toArray := #[], valid := ⋯ } }

@[reducible, inline]

abbrev Array.PrefixTable.size {α : Type u_1} (t : Array.PrefixTable α) : Nat

Returns the size of the prefix table

Equations

• t.size = t.size

@[irreducible]

def Array.PrefixTable.step {α : Type u_1} [BEq α] (t : Array.PrefixTable α) (x : α) : Fin (t.size + 1) → Fin (t.size + 1)

Transition function for the KMP matcher

Assuming we have an input xs with a suffix that matches the pattern prefix t.pattern[:len] where len : Fin (t.size+1). Then xs.push x has a suffix that matches the pattern prefix t.pattern[:t.step x len]. If len is as large as possible then t.step x len will also be as large as possible.

Equations

• One or more equations did not get rendered due to their size.
• t.step x ⟨0, hk_2⟩ = if h : 0 < t.size then if (x == t.toArray[0].fst) = true then ⟨0 + 1, ⋯⟩ else (fun (x : Unit) => ⟨0, ⋯⟩) () else (fun (x : Unit) => ⟨0, ⋯⟩) ()

def Array.PrefixTable.extend {α : Type u_1} [BEq α] (t : Array.PrefixTable α) (x : α) : Array.PrefixTable α

Extend a prefix table by one element

If t is the prefix table for xs then t.extend x is the prefix table for xs.push x.

Equations

• t.extend x = { toArray := t.push (x, ↑(t.step x ⟨t.size, ⋯⟩)), valid := ⋯ }

def Array.mkPrefixTable {α : Type u_1} [BEq α] (xs : Array α) : Array.PrefixTable α

Make prefix table from a pattern array

Equations

• xs.mkPrefixTable = Array.foldl (fun (x : Array.PrefixTable α) => x.extend) default xs

def Array.mkPrefixTableOfStream {α : Type u_1} {σ : Type u_2} [BEq α] [Stream σ α] (stream : σ) : Array.PrefixTable α

Make prefix table from a pattern stream

Equations

• Array.mkPrefixTableOfStream stream = Array.mkPrefixTableOfStream.loop default stream

partial def Array.mkPrefixTableOfStream.loop {α : Type u_1} {σ : Type u_2} [BEq α] [Stream σ α] (t : Array.PrefixTable α) (stream : σ) : Array.PrefixTable α

Inner loop for mkPrefixTableOfStream

structure Array.Matcher (α : Type u_1) : Type u_1

KMP matcher structure

• table : Array.PrefixTable α

  Prefix table for the pattern

• state : Fin (self.table.size + 1)

  Current longest matching prefix

def Array.Matcher.ofArray {α : Type u_1} [BEq α] (pat : Array α) : Array.Matcher α

Make a KMP matcher for a given pattern array

Equations

• Array.Matcher.ofArray pat = { table := pat.mkPrefixTable, state := 0 }

def Array.Matcher.ofStream {α : Type u_1} {σ : Type u_2} [BEq α] [Stream σ α] (pat : σ) : Array.Matcher α

Make a KMP matcher for a given a pattern stream

Equations

• Array.Matcher.ofStream pat = { table := Array.mkPrefixTableOfStream pat, state := 0 }

partial def Array.Matcher.next? {α : Type u_1} {σ : Type u_2} [BEq α] [Stream σ α] (m : Array.Matcher α) (stream : σ) : Option (σ × Array.Matcher α)

Find next match from a given stream

Runs the stream until it reads a sequence that matches the sought pattern, then returns the stream state at that point and an updated matcher state.