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.

Equations

• List.Matcher.ofList pattern = { toMatcher := Array.Matcher.ofStream pattern, pattern := pattern }

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

List stream that keeps count of items read.

Equations

• List.instStreamProdNat_batteries α = { next? := fun (x : List α × Nat) => match x with | ([], snd) => none | (x :: xs, n) => some (x, xs, n + 1) }

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.

Equations

• m.findAll l = List.Matcher.findAll.loop m (l, 0) m.toMatcher #[]

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.

Equations

• m.find? l = match m.next? (l, 0) with | none => none | some (l, snd) => some (l.snd - m.table.size, l.snd)

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

Equations

• l.findAllInfix pattern = (List.Matcher.ofList pattern).findAll l

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

Equations

• l.findInfix? pattern = (List.Matcher.ofList pattern).find? l

@[inline]

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

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

Equations

• l.containsInfix pattern = (l.findInfix? pattern).isSome