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 did not match the pattern.

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

class String.Slice.Pattern.ToForwardSearcher (ρ : Type) (σ : 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.

• toSearcher (s : Slice) (pat : ρ) : 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.

class String.Slice.Pattern.ForwardPattern (ρ : Type) : Type

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

While these operations can be implemented on top of ToForwardSearcher some patterns allow for more efficient implementations. This class can be used to specialize for them. If there is no need to specialize in this fashion, then ForwardPattern.defaultImplementation can be used to automatically derive an instance.

• startsWith : Slice → ρ → Bool

  Checks whether the slice starts with the pattern.

• 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.

@[extern lean_slice_memcmp]

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

Equations

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

@[inline]

def String.Slice.Pattern.Internal.nextMatch {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] {s : Slice} (searcher : Std.Iter (SearchStep s)) : Option (Std.Iter (SearchStep s) × s.Pos × s.Pos)

Tries to skip the searcher until the next SearchStep.matched and return it. If no match is found until the end returns none.

Equations

• String.Slice.Pattern.Internal.nextMatch searcher = String.Slice.Pattern.Internal.nextMatch.go✝ searcher

@[inline]

def String.Slice.Pattern.Internal.nextReject {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] {s : Slice} (searcher : Std.Iter (SearchStep s)) : Option (Std.Iter (SearchStep s) × s.Pos × s.Pos)

Tries to skip the searcher until the next SearchStep.rejected and return it. If no reject is found until the end returns none.

Equations

• String.Slice.Pattern.Internal.nextReject searcher = String.Slice.Pattern.Internal.nextReject.go✝ searcher

@[specialize #[5]]

def String.Slice.Pattern.ForwardPattern.defaultStartsWith {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (SearchStep s)] [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Bool

Equations

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

@[specialize #[5]]

def String.Slice.Pattern.ForwardPattern.defaultDropPrefix? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (SearchStep s)] [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Option s.Pos

Equations

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

@[inline]

def String.Slice.Pattern.ForwardPattern.defaultImplementation {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (SearchStep s)] [ToForwardSearcher ρ σ] : ForwardPattern ρ

Equations

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

class String.Slice.Pattern.ToBackwardSearcher (ρ : Type) (σ : 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.

• toSearcher (s : Slice) (pat : ρ) : 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.

class String.Slice.Pattern.BackwardPattern (ρ : Type) : Type

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

While these operations can be implemented on top of ToBackwardSearcher, some patterns allow for more efficient implementations. This class can be used to specialize for them. If there is no need to specialize in this fashion, then BackwardPattern.defaultImplementation can be used to automatically derive an instance.

• endsWith : Slice → ρ → Bool

  Checks whether the slice ends with the pattern.

• 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.

@[specialize #[5]]

def String.Slice.Pattern.ToBackwardSearcher.defaultEndsWith {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (SearchStep s)] [ToBackwardSearcher ρ σ] (s : Slice) (pat : ρ) : Bool

Equations

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

@[specialize #[5]]

def String.Slice.Pattern.ToBackwardSearcher.defaultDropSuffix? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (SearchStep s)] [ToBackwardSearcher ρ σ] (s : Slice) (pat : ρ) : Option s.Pos

Equations

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

@[inline]

def String.Slice.Pattern.ToBackwardSearcher.defaultImplementation {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (SearchStep s)] [ToBackwardSearcher ρ σ] : BackwardPattern ρ

Equations

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