source
structure String.Matcher extends 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

  The pattern for the matcher

Instances For

source
@[inline]
def String.Matcher.ofSubstring (pattern : Substring) :
Matcher

Make KMP matcher from pattern substring

Equations

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

Instances For

source
@[inline]
def String.Matcher.ofString (pattern : String) :
Matcher

Make KMP matcher from pattern string

Equations

- String.Matcher.ofString pattern = String.Matcher.ofSubstring pattern.toSubstring

Instances For

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

Instances For

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

Find all substrings of `s` matching `m.pattern`.

Equations

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

Instances For

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

Accumulator loop for `String.Matcher.findAll`

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

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 }

Instances For

source
@[inline]
def Substring.findAllSubstr (s pattern : Substring) :
Array Substring

Returns all the substrings of `s` that match `pattern`.

Equations

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

Instances For

source
@[inline]
def Substring.findSubstr? (s pattern : Substring) :
Option Substring

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

Instances For

source
@[inline]
def Substring.containsSubstr (s pattern : Substring) :
Bool

Returns true iff `pattern` occurs as a substring of `s`.

Equations

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

Instances For

source
@[reducible, inline]
abbrev String.findAllSubstr (s : String) (pattern : Substring) :
Array Substring

Returns all the substrings of `s` that match `pattern`.

Equations

- s.findAllSubstr pattern = (String.Matcher.ofSubstring pattern).findAll s.toSubstring

Instances For

source
@[reducible, inline]
abbrev String.findSubstr? (s : String) (pattern : Substring) :
Option Substring

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

Equations

- s.findSubstr? pattern = s.toSubstring.findSubstr? pattern

Instances For

source
@[reducible, inline]
abbrev String.containsSubstr (s : String) (pattern : Substring) :
Bool

Returns true iff `pattern` occurs as a substring of `s`.

Equations

- s.containsSubstr pattern = s.toSubstring.containsSubstr pattern

Instances For