structure String.Matcherextends Array.Matcher Char : Type

Knuth-Morris-Pratt matcher type

This type is used to keep data for running the Knuth-Morris-Pratt (KMP) string matching algorithm. KMP is a linear time algorithm to locate all substrings of a string 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 different strings.

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

def m := Matcher.ofString "abba"

#eval Option.isSome <| m.find? "AbbabbA" -- false
#eval Option.isSome <| m.find? "aabbaa" -- true

#eval Array.size <| m.findAll "abbabba" -- 2
#eval Array.size <| m.findAll "abbabbabba" -- 3

• table : PrefixTable Char
• state : Fin (self.table.size + 1)
• pattern : Substring.Raw

  The pattern for the matcher

@[inline]

def String.Matcher.ofSubstring (pattern : Substring.Raw) : Matcher

Make KMP matcher from pattern substring

Equations

• String.Matcher.ofSubstring pattern = { toMatcher := Array.Matcher.ofStream pattern, pattern := pattern }

@[inline]

def String.Matcher.ofString (pattern : String) : Matcher

Make KMP matcher from pattern string

Equations

• String.Matcher.ofString pattern = String.Matcher.ofSubstring pattern.toRawSubstring

@[reducible, inline]

abbrev String.Matcher.patternSize (m : Matcher) : Nat

The byte size of the string pattern for the matcher

Equations

• m.patternSize = m.pattern.bsize

def String.Matcher.findAll (m : Matcher) (s : Substring.Raw) : Array Substring.Raw

Find all substrings of s matching m.pattern.

Equations

• m.findAll s = String.Matcher.findAll.loop m s m.toMatcher #[]

partial def String.Matcher.findAll.loop (m : Matcher) (s : Substring.Raw) (am : Array.Matcher Char) (occs : Array Substring.Raw) : Array Substring.Raw

Accumulator loop for String.Matcher.findAll

def String.Matcher.find? (m : Matcher) (s : Substring.Raw) : Option Substring.Raw

Find the first substring of s matching m.pattern, or none if no such substring exists.

Equations

• m.find? s = match m.next? s with | none => none | some (s, snd) => some { str := s.str, startPos := { byteIdx := s.startPos.byteIdx - m.patternSize }, stopPos := s.startPos }

@[inline]

def Substring.Raw.findAllSubstr (s pattern : Raw) : Array Raw

Returns all the substrings of s that match pattern.

Equations

• s.findAllSubstr pattern = (String.Matcher.ofSubstring pattern).findAll s

@[inline]

def Substring.Raw.findSubstr? (s pattern : Raw) : Option Raw

Returns the first substring of s that matches pattern, or none if there is no such substring.

Equations

• s.findSubstr? pattern = (String.Matcher.ofSubstring pattern).find? s

@[inline]

def Substring.Raw.containsSubstr (s pattern : Raw) : Bool

Returns true iff pattern occurs as a substring of s.

Equations

• s.containsSubstr pattern = (s.findSubstr? pattern).isSome

@[reducible, inline, deprecated Substring.Raw.findAllSubstr (since := "2025-11-16")]

abbrev Substring.findAllSubstr (s pattern : Raw) : Array Raw

Returns all the substrings of s that match pattern.

Equations

• Substring.findAllSubstr = Substring.Raw.findAllSubstr

@[reducible, inline, deprecated Substring.Raw.findSubstr? (since := "2025-11-16")]

abbrev Substring.findSubstr? (s pattern : Raw) : Option Raw

Returns the first substring of s that matches pattern, or none if there is no such substring.

Equations

• Substring.findSubstr? = Substring.Raw.findSubstr?

@[reducible, inline, deprecated Substring.Raw.containsSubstr (since := "2025-11-16")]

abbrev Substring.containsSubstr (s pattern : Raw) : Bool

Returns true iff pattern occurs as a substring of s.

Equations

• Substring.containsSubstr = Substring.Raw.containsSubstr

@[reducible, inline]

abbrev String.findAllSubstr (s : String) (pattern : Substring.Raw) : Array Substring.Raw

Returns all the substrings of s that match pattern.

Equations

• s.findAllSubstr pattern = (String.Matcher.ofSubstring pattern).findAll s.toRawSubstring

@[reducible, inline]

abbrev String.findSubstr? (s : String) (pattern : Substring.Raw) : Option Substring.Raw

Returns the first substring of s that matches pattern, or none if there is no such substring.

Equations

• s.findSubstr? pattern = s.toRawSubstring.findSubstr? pattern

@[reducible, inline]

abbrev String.containsSubstr (s : String) (pattern : Substring.Raw) : Bool

Returns true iff pattern occurs as a substring of s.

Equations

• s.containsSubstr pattern = s.toRawSubstring.containsSubstr pattern