source
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

Instances For

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

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

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

Returns the size of the prefix table

Equations

- t.size = t.size

Instances For

source
@[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.

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, ⋯⟩) ()

Instances For

source
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`.

Equations

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

Instances For

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

Make prefix table from a pattern array

Equations

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

Instances For

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

Make prefix table from a pattern stream

Equations

- Array.mkPrefixTableOfStream stream = Array.mkPrefixTableOfStream.loop default stream

Instances For

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

Inner loop for `mkPrefixTableOfStream`

source
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

Instances For

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

Make a KMP matcher for a given pattern array

Equations

- Array.Matcher.ofArray pat = { table := pat.mkPrefixTable }

Instances For

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

Make a KMP matcher for a given a pattern stream

Equations

- Array.Matcher.ofStream pat = { table := Array.mkPrefixTableOfStream pat }

Instances For

source
partial def Array.Matcher.next? {α : Type u_1} {σ : Type u_2} [BEq α] [Std.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.

source
structure Array.Matcher.Iterator (σ : Type u_1) (n : Type u_1 → Type u_2) (α : Type u_1) [BEq α] (m : Matcher α) [Std.Iterators.Iterator σ n α] :
Type u_1

Iterator transformer for KMP matcher.

- inner : Std.IterM n α

  Inner iterator.

- state : Fin (m.table.size + 1)

  Matcher state.

Instances For

source
def Array.Matcher.modifyStep {α σ : Type u_1} {n : Type u_1 → Type u_2} [BEq α] (m : Matcher α) [Std.Iterators.Iterator σ n α] (it : Std.IterM n σ) :
it.internalState.inner.Step → Std.Iterators.IterStep (Std.IterM n σ) σ

Implementation datail for `Matcher.Iterator`.

Equations

- One or more equations did not get rendered due to their size.
- m.modifyStep it ⟨Std.Iterators.IterStep.done, property⟩ = Std.Iterators.IterStep.done

Instances For

source
instance Array.Matcher.instIteratorIteratorOfMonad {n : Type u_1 → Type u_2} {α σ : Type u_1} [Monad n] [BEq α] (m : Matcher α) [Std.Iterators.Iterator σ n α] :
Std.Iterators.Iterator (Matcher.Iterator σ n α m) n σ
Equations

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

source
instance Array.Matcher.instFiniteIterator {n : Type u_1 → Type u_2} {α σ : Type u_1} [Monad n] [BEq α] (m : Matcher α) [Std.Iterators.Iterator σ n α] [inst : Std.Iterators.Finite σ n] :
Std.Iterators.Finite (Matcher.Iterator σ n α m) n