structure Array.PrefixTable (α : Type u_1) extends Array (α × Nat) : 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

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

@[reducible, inline]

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

Returns the size of the prefix table

@[irreducible]

def Array.PrefixTable.step {α : Type u_1} [BEq α] (t : 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.

def Array.PrefixTable.extend {α : Type u_1} [BEq α] (t : PrefixTable α) (x : α) : 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.

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

Make prefix table from a pattern array

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

Make prefix table from a pattern stream

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

Inner loop for mkPrefixTableOfStream

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

KMP matcher structure

• table : 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 α) : Matcher α

Make a KMP matcher for a given pattern array

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

Make a KMP matcher for a given a pattern stream

partial def Array.Matcher.next? {α : Type u_1} {σ : Type u_2} [BEq α] [Stream σ α] (m : Matcher α) (stream : σ) : Option (σ × 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.