inductive String.Slice.Pattern.SearchStep (s : Slice) : Type

A step taken during the traversal of a Slice by a forward or backward searcher.

• rejected {s : Slice} (startPos endPos : s.Pos) : SearchStep s

  The subslice starting at startPos and ending at endPos did not match the pattern.

• matched {s : Slice} (startPos endPos : s.Pos) : SearchStep s

  The subslice starting at startPos and ending at endPos matches the pattern.

@[instance_reducible]

instance String.Slice.Pattern.instInhabitedSearchStep {a✝ : Slice} : Inhabited (SearchStep a✝)

Equations

• String.Slice.Pattern.instInhabitedSearchStep = { default := String.Slice.Pattern.instInhabitedSearchStep.default }

def String.Slice.Pattern.instInhabitedSearchStep.default {a✝ : Slice} : SearchStep a✝

Equations

• String.Slice.Pattern.instInhabitedSearchStep.default = String.Slice.Pattern.SearchStep.rejected default default

def String.Slice.Pattern.instBEqSearchStep.beq {s✝ : Slice} : SearchStep s✝ → SearchStep s✝ → Bool

Equations

• String.Slice.Pattern.instBEqSearchStep.beq (String.Slice.Pattern.SearchStep.rejected a a_1) (String.Slice.Pattern.SearchStep.rejected b b_1) = (a == b && a_1 == b_1)
• String.Slice.Pattern.instBEqSearchStep.beq (String.Slice.Pattern.SearchStep.matched a a_1) (String.Slice.Pattern.SearchStep.matched b b_1) = (a == b && a_1 == b_1)
• String.Slice.Pattern.instBEqSearchStep.beq x✝¹ x✝ = false

@[instance_reducible]

instance String.Slice.Pattern.instBEqSearchStep {s✝ : Slice} : BEq (SearchStep s✝)

Equations

• String.Slice.Pattern.instBEqSearchStep = { beq := String.Slice.Pattern.instBEqSearchStep.beq }

@[inline]

def String.Slice.Pattern.SearchStep.startPos {s : Slice} (st : SearchStep s) : s.Pos

The start position of a SearchStep.

Equations

• (String.Slice.Pattern.SearchStep.rejected startPos endPos).startPos = startPos
• (String.Slice.Pattern.SearchStep.matched startPos endPos).startPos = startPos

@[simp]

theorem String.Slice.Pattern.SearchStep.startPos_rejected {s : Slice} {p q : s.Pos} : (rejected p q).startPos = p

@[simp]

theorem String.Slice.Pattern.SearchStep.startPos_matched {s : Slice} {p q : s.Pos} : (matched p q).startPos = p

@[inline]

def String.Slice.Pattern.SearchStep.endPos {s : Slice} (st : SearchStep s) : s.Pos

The end position of a SearchStep.

Equations

• (String.Slice.Pattern.SearchStep.rejected startPos endPos).endPos = endPos
• (String.Slice.Pattern.SearchStep.matched startPos endPos).endPos = endPos

@[simp]

theorem String.Slice.Pattern.SearchStep.endPos_rejected {s : Slice} {p q : s.Pos} : (rejected p q).endPos = q

@[simp]

theorem String.Slice.Pattern.SearchStep.endPos_matched {s : Slice} {p q : s.Pos} : (matched p q).endPos = q

def String.Slice.Pattern.SearchStep.ofSliceFrom {s : Slice} {p : s.Pos} (st : SearchStep (s.sliceFrom p)) : SearchStep s

Converts a SearchStep (s.sliceFrom p) into a SearchStep s by applying Slice.Pos.ofSliceFrom to the start and end position.

Equations

• (String.Slice.Pattern.SearchStep.rejected l r).ofSliceFrom = String.Slice.Pattern.SearchStep.rejected (String.Slice.Pos.ofSliceFrom l) (String.Slice.Pos.ofSliceFrom r)
• (String.Slice.Pattern.SearchStep.matched l r).ofSliceFrom = String.Slice.Pattern.SearchStep.matched (String.Slice.Pos.ofSliceFrom l) (String.Slice.Pos.ofSliceFrom r)

@[simp]

theorem String.Slice.Pattern.SearchStep.startPos_ofSliceFrom {s : Slice} {p : s.Pos} {st : SearchStep (s.sliceFrom p)} : st.ofSliceFrom.startPos = Pos.ofSliceFrom st.startPos

@[simp]

theorem String.Slice.Pattern.SearchStep.endPos_ofSliceFrom {s : Slice} {p : s.Pos} {st : SearchStep (s.sliceFrom p)} : st.ofSliceFrom.endPos = Pos.ofSliceFrom st.endPos

class String.Slice.Pattern.ForwardPattern {ρ : Type} (pat : ρ) : Type

Provides simple pattern matching capabilities from the start of a Slice.

• dropPrefix? (s : Slice) : Option s.Pos

  Checks whether the slice starts with the pattern. If it does, the slice is returned with the prefix removed; otherwise the result is none.

• dropPrefixOfNonempty? (s : Slice) (h : s.isEmpty = false) : Option s.Pos

  Checks whether the slice starts with the pattern. If it does, the slice is returned with the prefix removed; otherwise the result is none.

• startsWith (s : Slice) : Bool

  Checks whether the slice starts with the pattern.

class String.Slice.Pattern.LawfulForwardPattern {ρ : Type} (pat : ρ) [ForwardPattern pat] : Prop

A lawful forward pattern is one where the three functions ForwardPattern.dropPrefix?, ForwardPattern.dropPrefixOfNonempty? and ForwardPattern.startsWith agree for any given input slice.

Note that this is a relatively weak condition. It is non-uniform in the sense that the functions can still return completely different results on different slices, even if they represent the same string.

There is a stronger lawfulness typeclass LawfulForwardPatternModel that asserts that the ForwardPattern.dropPrefix? function behaves like a function that drops the longest prefix according to some notion of matching.

• dropPrefixOfNonempty?_eq {s : Slice} (h : s.isEmpty = false) : ForwardPattern.dropPrefixOfNonempty? pat s h = ForwardPattern.dropPrefix? pat s
• startsWith_eq (s : Slice) : ForwardPattern.startsWith pat s = (ForwardPattern.dropPrefix? pat s).isSome

class String.Slice.Pattern.StrictForwardPattern {ρ : Type} (pat : ρ) [ForwardPattern pat] : Prop

A strict forward pattern is one which never drops an empty prefix.

This condition ensures that the default searcher derived from the forward pattern is a finite iterator.

• ne_startPos {s : Slice} (h : s.isEmpty = false) (q : s.Pos) : ForwardPattern.dropPrefixOfNonempty? pat s h = some q → q ≠ s.startPos

class String.Slice.Pattern.ToForwardSearcher {ρ : Type} (pat : ρ) (σ : outParam (Slice → Type)) : Type

Provides a conversion from a pattern to an iterator of SearchStep that searches for matches of the pattern from the start towards the end of a Slice.

While these operations can be implemented on top of ForwardPattern, some patterns allow for more efficient implementations. For example, a searcher for String patterns derived from the ForwardPattern instance on strings would try to match the pattern at every position in the string, but more efficient string matching routines are known. Indeed, the Lean standard library uses the Knuth-Morris-Pratt algorithm. See the module Init.Data.String.Pattern.String for the implementation.

This class can be used to provide such an efficient implementation. If there is no need to specialize in this fashion, then ToForwardSearcher.defaultImplementation can be used to automatically derive an instance.

• toSearcher (s : Slice) : Std.Iter (SearchStep s)

  Builds an iterator of SearchStep corresponding to matches of pat along the slice s. The SearchSteps returned by this iterator must contain ranges that are adjacent, non-overlapping and cover all of s.

structure String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher {ρ : Type} (pat : ρ) (s : Slice) : Type

• currPos : s.Pos

def String.Slice.Pattern.ToForwardSearcher.instInhabitedDefaultForwardSearcher.default {a✝ : Type} {a✝¹ : a✝} {a✝² : Slice} : DefaultForwardSearcher a✝¹ a✝²

Equations

• String.Slice.Pattern.ToForwardSearcher.instInhabitedDefaultForwardSearcher.default = { currPos := default }

@[instance_reducible]

instance String.Slice.Pattern.ToForwardSearcher.instInhabitedDefaultForwardSearcher {a✝ : Type} {a✝¹ : a✝} {a✝² : Slice} : Inhabited (DefaultForwardSearcher a✝¹ a✝²)

Equations

• String.Slice.Pattern.ToForwardSearcher.instInhabitedDefaultForwardSearcher = { default := String.Slice.Pattern.ToForwardSearcher.instInhabitedDefaultForwardSearcher.default }

@[inline]

def String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.iter {ρ : Type} (pat : ρ) (s : Slice) : Std.Iter (SearchStep s)

Equations

• String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.iter pat s = { internalState := { currPos := s.startPos } }

@[instance_reducible]

instance String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.instIteratorIdSearchStepOfForwardPattern {ρ : Type} (pat : ρ) (s : Slice) [ForwardPattern pat] : Std.Iterator (DefaultForwardSearcher pat s) Id (SearchStep s)

Equations

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

instance String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.instFiniteIdSearchStepOfStrictForwardPattern {ρ : Type} (pat : ρ) {s : Slice} [ForwardPattern pat] [StrictForwardPattern pat] : Std.Iterators.Finite (DefaultForwardSearcher pat s) Id

@[instance_reducible]

instance String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.instIteratorLoopIdSearchStep {ρ : Type} (pat : ρ) {s : Slice} [ForwardPattern pat] : Std.IteratorLoop (DefaultForwardSearcher pat s) Id Id

Equations

• String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.instIteratorLoopIdSearchStep pat = Std.IteratorLoop.defaultImplementation

@[inline]

def String.Slice.Pattern.ToForwardSearcher.defaultImplementation {ρ✝ : Type} {pat : ρ✝} [ForwardPattern pat] : ToForwardSearcher pat (DefaultForwardSearcher pat)

The default implementation of ToForwardSearcher repeatedly tries to match the pattern using the given ForwardPattern instance.

It is sometimes possible to give a more efficient implementation; see ToForwardSearcher for more details.

Equations

• String.Slice.Pattern.ToForwardSearcher.defaultImplementation = { toSearcher := String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.iter pat }

@[extern lean_string_memcmp]

def String.Slice.Pattern.Internal.memcmpStr (lhs rhs : String) (lstart rstart len : Pos.Raw) (h1 : len.offsetBy lstart ≤ lhs.rawEndPos) (h2 : len.offsetBy rstart ≤ rhs.rawEndPos) : Bool

Equations

• String.Slice.Pattern.Internal.memcmpStr lhs rhs lstart rstart len h1 h2 = String.Slice.Pattern.Internal.memcmpStr.go✝ lhs rhs lstart rstart len h1 h2 0

@[inline]

def String.Slice.Pattern.Internal.memcmpSlice (lhs rhs : Slice) (lstart rstart len : Pos.Raw) (h1 : len.offsetBy lstart ≤ lhs.rawEndPos) (h2 : len.offsetBy rstart ≤ rhs.rawEndPos) : Bool

Equations

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

class String.Slice.Pattern.BackwardPattern {ρ : Type} (pat : ρ) : Type

Provides simple pattern matching capabilities from the end of a Slice.

• dropSuffix? (s : Slice) : Option s.Pos

  Checks whether the slice ends with the pattern. If it does, the slice is returned with the suffix removed; otherwise the result is none.

• dropSuffixOfNonempty? (s : Slice) (h : s.isEmpty = false) : Option s.Pos

  Checks whether the slice ends with the pattern. If it does, the slice is returned with the suffix removed; otherwise the result is none.

• endsWith : Slice → Bool

  Checks whether the slice ends with the pattern.

class String.Slice.Pattern.LawfulBackwardPattern {ρ : Type} (pat : ρ) [BackwardPattern pat] : Prop

A lawful backward pattern is one where the three functions BackwardPattern.dropSuffix?, BackwardPattern.dropSuffixOfNonempty? and BackwardPattern.endsWith agree for any given input slice.

Note that this is a relatively weak condition. It is non-uniform in the sense that the functions can still return completely different results on different slices, even if they represent the same string.

There is a stronger lawfulness typeclass LawfulBackwardPatternModel that asserts that the BackwardPattern.dropSuffix? function behaves like a function that drops the longest prefix according to some notion of matching.

• dropSuffixOfNonempty?_eq {s : Slice} (h : s.isEmpty = false) : BackwardPattern.dropSuffixOfNonempty? pat s h = BackwardPattern.dropSuffix? pat s
• endsWith_eq (s : Slice) : BackwardPattern.endsWith pat s = (BackwardPattern.dropSuffix? pat s).isSome

class String.Slice.Pattern.StrictBackwardPattern {ρ : Type} (pat : ρ) [BackwardPattern pat] : Prop

A strict backward pattern is one which never drops an empty suffix.

This condition ensures that the default searcher derived from the backward pattern is a finite iterator.

• ne_endPos {s : Slice} (h : s.isEmpty = false) (q : s.Pos) : BackwardPattern.dropSuffixOfNonempty? pat s h = some q → q ≠ s.endPos

class String.Slice.Pattern.ToBackwardSearcher {ρ : Type} (pat : ρ) (σ : outParam (Slice → Type)) : Type

Provides a conversion from a pattern to an iterator of SearchStep searching for matches of the pattern from the end towards the start of a Slice.

While these operations can be implemented on top of BackwardPattern, some patterns allow for more efficient implementations. For example, a searcher for String patterns derived from the BackwardPattern instance on strings would try to match the pattern at every position in the string, but more efficient string matching routines are known. Indeed, the Lean standard library uses the Knuth-Morris-Pratt algorithm. See the module Init.Data.String.Pattern.String for the implementation.

This class can be used to provide such an efficient implementation. If there is no need to specialize in this fashion, then ToBackwardSearcher.defaultImplementation can be used to automatically derive an instance.

• toSearcher (s : Slice) : Std.Iter (SearchStep s)

  Build an iterator of SearchStep corresponding to matches of pat along the slice s. The SearchSteps returned by this iterator must contain ranges that are adjacent, non-overlapping and cover all of s.

structure String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher {ρ : Type} (pat : ρ) (s : Slice) : Type

• currPos : s.Pos

def String.Slice.Pattern.ToBackwardSearcher.instInhabitedDefaultBackwardSearcher.default {a✝ : Type} {a✝¹ : a✝} {a✝² : Slice} : DefaultBackwardSearcher a✝¹ a✝²

Equations

• String.Slice.Pattern.ToBackwardSearcher.instInhabitedDefaultBackwardSearcher.default = { currPos := default }

@[instance_reducible]

instance String.Slice.Pattern.ToBackwardSearcher.instInhabitedDefaultBackwardSearcher {a✝ : Type} {a✝¹ : a✝} {a✝² : Slice} : Inhabited (DefaultBackwardSearcher a✝¹ a✝²)

Equations

• String.Slice.Pattern.ToBackwardSearcher.instInhabitedDefaultBackwardSearcher = { default := String.Slice.Pattern.ToBackwardSearcher.instInhabitedDefaultBackwardSearcher.default }

@[inline]

def String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.iter {ρ : Type} (pat : ρ) (s : Slice) : Std.Iter (SearchStep s)

Equations

• String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.iter pat s = { internalState := { currPos := s.endPos } }

@[instance_reducible]

instance String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.instIteratorIdSearchStepOfBackwardPattern {ρ : Type} (pat : ρ) (s : Slice) [BackwardPattern pat] : Std.Iterator (DefaultBackwardSearcher pat s) Id (SearchStep s)

Equations

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

instance String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.instFiniteIdSearchStepOfStrictBackwardPattern {ρ : Type} (pat : ρ) {s : Slice} [BackwardPattern pat] [StrictBackwardPattern pat] : Std.Iterators.Finite (DefaultBackwardSearcher pat s) Id

@[instance_reducible]

instance String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.instIteratorLoopIdSearchStep {ρ : Type} (pat : ρ) {s : Slice} [BackwardPattern pat] : Std.IteratorLoop (DefaultBackwardSearcher pat s) Id Id

Equations

• String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.instIteratorLoopIdSearchStep pat = Std.IteratorLoop.defaultImplementation

@[inline]

def String.Slice.Pattern.ToBackwardSearcher.defaultImplementation {ρ✝ : Type} {pat : ρ✝} [BackwardPattern pat] : ToBackwardSearcher pat (DefaultBackwardSearcher pat)

The default implementation of ToBackwardSearcher repeatedly tries to match the pattern using the given BackwardPattern instance.

It is sometimes possible to give a more efficient implementation; see ToBackwardSearcher for more details.

Equations

• String.Slice.Pattern.ToBackwardSearcher.defaultImplementation = { toSearcher := String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.iter pat }