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

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

  Validity condition to help with termination proofs

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.

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

Equations

• Array.instInhabitedPrefixTable = { default := { toArray := #[], valid := (_ : ∀ {i : Nat} (a : i < Array.size #[]), #[][i].snd ≤ i) } }

@[inline, reducible]

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

Returns the size of the prefix table

Equations

• Array.PrefixTable.size t = Array.size t.toArray

def Array.PrefixTable.step {α : Type u_1} [BEq α] (t : Array.PrefixTable α) (x : α) : Fin (Array.PrefixTable.size t + 1) → Fin (Array.PrefixTable.size t + 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.

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

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

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

Make prefix table from a pattern array

Equations

• Array.mkPrefixTable xs = Array.foldl (fun x => Array.PrefixTable.extend x) default xs 0 (Array.size 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

• table : Array.PrefixTable α

  Prefix table for the pattern

• state : Fin (Array.PrefixTable.size s.table + 1)

  Current longest matching prefix

KMP matcher structure

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 := Array.mkPrefixTable pat, 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.