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

Instances For

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

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

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

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

Instances For

source
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

Instances For

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

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

source
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 `SearchStep`s returned by this iterator must contain ranges that are adjacent, non-overlapping and cover all of `s`.

Instances

source
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`.

Instances

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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 `SearchStep`s returned by this iterator must contain ranges that are adjacent, non-overlapping and cover all of `s`.

Instances

source
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`.

Instances

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

Instances For

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

Instances For

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

Instances For