# Documentation

Std.Data.Array.Match

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

Instances For
@[inline, reducible]
abbrev Array.PrefixTable.size {α : Type u_1} (t : ) :

Returns the size of the prefix table

Instances For
def Array.PrefixTable.step {α : Type u_1} [BEq α] (t : ) (x : α) :
Fin ()Fin ()

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

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.

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

Make prefix table from a pattern array

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

Make prefix table from a pattern stream

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

Inner loop for mkPrefixTableOfStream

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

KMP matcher structure

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

Make a KMP matcher for a given pattern array

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

Make a KMP matcher for a given a pattern stream

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

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.