instance instCoeStringSubstring : Coe String Substring

Equations

• instCoeStringSubstring = { coe := String.toSubstring }

theorem String.Pos.ne_zero_of_lt {a : String.Pos} {b : String.Pos} : a < b → b ≠ 0

structure String.Matcherextends Array.Matcher : 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 : Array.PrefixTable Char
• state : Fin (Array.PrefixTable.size self.toMatcher.table + 1)
• pattern : Substring

  The pattern for the matcher

@[inline]

def String.Matcher.ofSubstring (pattern : Substring) : String.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) : String.Matcher

Make KMP matcher from pattern string

Equations

• String.Matcher.ofString pattern = String.Matcher.ofSubstring (String.toSubstring pattern)

@[inline, reducible]

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

The byte size of the string pattern for the matcher

Equations

• String.Matcher.patternSize m = Substring.bsize m.pattern

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

Find all substrings of s matching m.pattern.

Equations

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

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

Accumulator loop for String.Matcher.findAll

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

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

Equations

• One or more equations did not get rendered due to their size.

def Substring.commonPrefix (s : Substring) (t : Substring) : Substring

Returns the longest common prefix of two substrings. The returned substring will use the same underlying string as s.

Equations

• Substring.commonPrefix s t = { str := s.str, startPos := s.startPos, stopPos := Substring.commonPrefix.loop s t s.startPos t.startPos }

def Substring.commonPrefix.loop (s : Substring) (t : Substring) (spos : String.Pos) (tpos : String.Pos) : String.Pos

Returns the ending position of the common prefix, working up from spos, tpos.

Equations

• One or more equations did not get rendered due to their size.

def Substring.commonSuffix (s : Substring) (t : Substring) : Substring

Returns the longest common suffix of two substrings. The returned substring will use the same underlying string as s.

Equations

• Substring.commonSuffix s t = { str := s.str, startPos := Substring.commonSuffix.loop s t s.stopPos t.stopPos, stopPos := s.stopPos }

def Substring.commonSuffix.loop (s : Substring) (t : Substring) (spos : String.Pos) (tpos : String.Pos) : String.Pos

Returns the starting position of the common prefix, working down from spos, tpos.

Equations

• One or more equations did not get rendered due to their size.

def Substring.dropPrefix? (s : Substring) (pre : Substring) : Option Substring

If pre is a prefix of s, i.e. s = pre ++ t, returns the remainder t.

Equations

• Substring.dropPrefix? s pre = let t := Substring.commonPrefix s pre; if Substring.bsize t = Substring.bsize pre then some { str := s.str, startPos := t.stopPos, stopPos := s.stopPos } else none

def Substring.dropSuffix? (s : Substring) (suff : Substring) : Option Substring

If suff is a suffix of s, i.e. s = t ++ suff, returns the remainder t.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Returns all the substrings of s that match pattern.

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

Returns true iff pattern occurs as a substring of s.

Equations

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

@[inline, reducible]

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

Returns all the substrings of s that match pattern.

Equations

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

@[inline, reducible]

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

• String.findSubstr? s pattern = Substring.findSubstr? (String.toSubstring s) pattern

@[inline, reducible]

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

Returns true iff pattern occurs as a substring of s.

Equations

• String.containsSubstr s pattern = Substring.containsSubstr (String.toSubstring s) pattern

def String.dropPrefix? (s : String) (pre : Substring) : Option Substring

If pre is a prefix of s, i.e. s = pre ++ t, returns the remainder t.

Equations

• String.dropPrefix? s pre = Substring.dropPrefix? (String.toSubstring s) pre

def String.dropSuffix? (s : String) (suff : Substring) : Option Substring

If suff is a suffix of s, i.e. s = t ++ suff, returns the remainder t.

Equations

• String.dropSuffix? s suff = Substring.dropSuffix? (String.toSubstring s) suff

def String.stripPrefix (s : String) (pre : Substring) : String

s.stripPrefix pre will remove pre from the beginning of s if it occurs there, or otherwise return s.

Equations

• String.stripPrefix s pre = Option.getD (Option.map Substring.toString (String.dropPrefix? s pre)) s

def String.stripSuffix (s : String) (suff : Substring) : String

s.stripSuffix suff will remove suff from the end of s if it occurs there, or otherwise return s.

Equations

• String.stripSuffix s suff = Option.getD (Option.map Substring.toString (String.dropSuffix? s suff)) s

def String.count (s : String) (c : Char) : Nat

Count the occurrences of a character in a string.

Equations

• String.count s c = String.foldl (fun (n : Nat) (d : Char) => if d = c then n + 1 else n) 0 s