Documentation

Batteries.Data.List.Matcher

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
@[inline]
def List.Matcher.ofList {α : Type u_1} [BEq α] (pattern : List α) :

Make KMP matcher from list pattern.

Equations

List stream that keeps count of items read.

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

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

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

Accumulator loop for List.Matcher.findAll

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

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

Equations
@[inline]
def List.findAllInfix {α : Type u_1} [BEq α] (l pattern : List α) :

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

Equations
@[inline]
def List.findInfix? {α : Type u_1} [BEq α] (l pattern : List α) :

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

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

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

Equations