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

Knuth-Morris-Pratt matcher type

This type is used to keep data for running the Knuth-Morris-Pratt (KMP) list matching algorithm. KMP is a linear time algorithm to locate all contiguous sublists of a list that match a given pattern. Generating the algorithm data is also linear in the length of the pattern but the data can be re-used to match the same pattern over multiple lists.

The KMP data for a pattern can be generated using Matcher.ofList. Then Matcher.find? and Matcher.findAll can be used to run the algorithm on an input list.

def m := Matcher.ofList [0,1,1,0]

#eval Option.isSome <| m.find? [2,1,1,0,1,1,2] -- false
#eval Option.isSome <| m.find? [0,0,1,1,0,0] -- true

#eval Array.size <| m.findAll [0,1,1,0,1,1,0] -- 2
#eval Array.size <| m.findAll [0,1,1,0,1,1,0,1,1,0] -- 3

• table : PrefixTable α
• state : Fin (self.table.size + 1)
• pattern : List α

  The pattern for the matcher

@[inline]

def List.Matcher.ofList {α : Type u_1} [BEq α] (pattern : List α) : Matcher α

Make KMP matcher from list pattern.

def List.instStreamProdNat_batteries (α : Type u_1) : Stream (List α × Nat) α

List stream that keeps count of items read.

def List.Matcher.findAll {α : Type u_1} [BEq α] (m : Matcher α) (l : List α) : Array (Nat × Nat)

Find all start and end positions of all infix sublists of l matching m.pattern. The sublists may be overlapping.

partial def List.Matcher.findAll.loop {α : Type u_1} [BEq α] (m : Matcher α) (l : List α × Nat) (am : Array.Matcher α) (occs : Array (Nat × Nat)) : Array (Nat × Nat)

Accumulator loop for List.Matcher.findAll

def List.Matcher.find? {α : Type u_1} [BEq α] (m : Matcher α) (l : List α) : Option (Nat × Nat)

Find the start and end positions of the first infix sublist of l matching m.pattern, or none if there is no such sublist.

@[inline]

def List.findAllInfix {α : Type u_1} [BEq α] (l pattern : List α) : Array (Nat × Nat)

Returns all the start and end positions of all infix sublists of of l that match pattern. The sublists may be overlapping.

@[inline]

def List.findInfix? {α : Type u_1} [BEq α] (l pattern : List α) : Option (Nat × Nat)

Returns the start and end positions of the first infix sublist of l that matches pattern, or none if there is no such sublist.

@[inline]

def List.containsInfix {α : Type u_1} [BEq α] (l pattern : List α) : Bool

Returns true iff pattern occurs as an infix sublist of l.