max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: derive string searcher from string pattern (#12312)

Browse source 
This PR reverses the relationship between the `ForwardPattern` and
`ToForwardSearcher` classes.

Previously, it was possible to derive `ForwardPattern` (i.e.,
`dropPrefix?`) from `ToForwardSearcher` (i.e., get an iterator of
`SearchStep (s)`). Now, we give the default instance in the other
direction: it is now possible to derive `ToForwardSearcher` from
`ForwardPattern`. Since it is usually much easier to provide
`ForwardPattern` than `ToForwardSearcher`, this means more shared code,
which pays off double since we will give a correctness proof for the
default implementation in an upcoming PR.

This PR also adds some string lemmas.
This commit is contained in:
Markus Himmel 2026-02-05 08:38:31 +01:00 • committed by GitHub
parent 75d7f7eb22
commit 54cba90dc5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
9 changed files with 673 additions and 341 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/Init/Data/String/Basic.lean
View file

@ -1502,6 +1502,20 @@ def Slice.Pos.toReplaceEnd {s : Slice} (p₀ : s.Pos) (pos : s.Pos) (h : pos ≤
theorem Slice.Pos.offset_sliceTo {s : Slice} {p₀ : s.Pos} {pos : s.Pos} {h : pos ≤ p₀} :
(sliceTo p₀ pos h).offset = pos.offset := (rfl)
@[simp]
theorem Slice.Pos.ofSliceTo_startPos {s : Slice} {pos : s.Pos} :
ofSliceTo (s.sliceTo pos).startPos = s.startPos := by
simp [Pos.ext_iff]
@[simp]
theorem Slice.Pos.ofSliceTo_endPos {s : Slice} {pos : s.Pos} :
ofSliceTo (s.sliceTo pos).endPos = pos := by
simp [Pos.ext_iff]
theorem Slice.Pos.ofSliceTo_inj {s : Slice} {p₀ : s.Pos} {pos pos' : (s.sliceTo p₀).Pos} :
ofSliceTo pos = ofSliceTo pos' ↔ pos = pos' := by
simp [Pos.ext_iff]
theorem Slice.Pos.copy_eq_append_get {s : Slice} {pos : s.Pos} (h : pos ≠ s.endPos) :
∃ t₁ t₂ : String, s.copy = t₁ ++ singleton (pos.get h) ++ t₂ ∧ t₁.utf8ByteSize = pos.offset.byteIdx := by
obtain ⟨t₂, ht₂⟩ := (s.sliceFrom pos).copy.eq_singleton_append (by simpa [← Pos.ofCopy_inj, ← ofSliceFrom_inj])
@ -2250,6 +2264,20 @@ def Pos.ofReplaceEnd {s : String} {p₀ : s.Pos} (pos : (s.sliceTo p₀).Pos) :
theorem Pos.offset_ofSliceTo {s : String} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} :
(ofSliceTo pos).offset = pos.offset := (rfl)
@[simp]
theorem Pos.ofSliceTo_startPos {s : String} {pos : s.Pos} :
ofSliceTo (s.sliceTo pos).startPos = s.startPos := by
simp [Pos.ext_iff]
@[simp]
theorem Pos.ofSliceTo_endPos {s : String} {pos : s.Pos} :
ofSliceTo (s.sliceTo pos).endPos = pos := by
simp [Pos.ext_iff]
theorem Pos.ofSliceTo_inj {s : String} {p₀ : s.Pos} {pos pos' : (s.sliceTo p₀).Pos} :
ofSliceTo pos = ofSliceTo pos' ↔ pos = pos' := by
simp [Pos.ext_iff, Slice.Pos.ext_iff]
@[simp]
theorem Pos.ofSliceTo_le {s : String} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} :
ofSliceTo pos ≤ p₀ := by

12
src/Init/Data/String/Defs.lean
View file

@ -630,6 +630,18 @@ def Slice.Pos.byte {s : Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : UInt8 :=
theorem push_eq_append (c : Char) : String.push s c = s ++ singleton c := by
simp
/--
Checks whether a slice is empty.
Empty slices have {name}`utf8ByteSize` {lean}`0`.
Examples:
* {lean}`"".toSlice.isEmpty = true`
* {lean}`" ".toSlice.isEmpty = false`
-/
@[inline]
def Slice.isEmpty (s : Slice) : Bool := s.utf8ByteSize == 0
@[deprecated String.toRawSubstring (since := "2025-11-18")]
def toSubstring (s : String) : Substring.Raw :=
s.toRawSubstring

1
src/Init/Data/String/Lemmas.lean
View file

@ -12,6 +12,7 @@ public import Init.Data.String.Lemmas.Search
public import Init.Data.String.Lemmas.FindPos
public import Init.Data.String.Lemmas.Basic
public import Init.Data.String.Lemmas.Order
public import Init.Data.String.Lemmas.IsEmpty
public import Init.Data.Char.Order
public import Init.Data.Char.Lemmas
public import Init.Data.List.Lex

133
src/Init/Data/String/Lemmas/IsEmpty.lean Normal file
View file

@ -0,0 +1,133 @@
/-
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
module
prelude
public import Init.Data.String.Basic
import all Init.Data.String.Defs
import Init.Data.String.Lemmas.Order
import Init.Data.String.Lemmas.Basic
import Init.Data.String.OrderInstances
import Init.Grind
public section
namespace String
namespace Slice
theorem isEmpty_eq {s : Slice} : s.isEmpty = (s.utf8ByteSize == 0) :=
(rfl)
theorem isEmpty_iff {s : Slice} :
s.isEmpty ↔ s.utf8ByteSize = 0 := by
simp [Slice.isEmpty_eq]
theorem startPos_eq_endPos_iff {s : Slice} :
s.startPos = s.endPos ↔ s.isEmpty := by
rw [eq_comm]
simp [Slice.Pos.ext_iff, Pos.Raw.ext_iff, Slice.isEmpty_iff]
theorem startPos_ne_endPos_iff {s : Slice} :
s.startPos ≠ s.endPos ↔ s.isEmpty = false := by
simp [Slice.startPos_eq_endPos_iff]
theorem startPos_ne_endPos {s : Slice} : s.isEmpty = false → s.startPos ≠ s.endPos :=
Slice.startPos_ne_endPos_iff.2
theorem isEmpty_iff_forall_eq {s : Slice} :
s.isEmpty ↔ ∀ (p q : s.Pos), p = q := by
rw [← Slice.startPos_eq_endPos_iff]
refine ⟨fun h p q => ?_, fun h => h _ _⟩
apply Std.le_antisymm
· apply Std.le_trans (Pos.le_endPos _) (h ▸ Pos.startPos_le _)
· apply Std.le_trans (Pos.le_endPos _) (h ▸ Pos.startPos_le _)
theorem isEmpty_eq_false_of_lt {s : Slice} {p q : s.Pos} :
p < q → s.isEmpty = false := by
rw [← Decidable.not_imp_not]
simp
rw [Slice.isEmpty_iff_forall_eq]
intro h
cases h p q
apply Std.lt_irrefl
@[simp]
theorem isEmpty_sliceFrom {s : Slice} {p : s.Pos} :
(s.sliceFrom p).isEmpty ↔ p = s.endPos := by
simp [← startPos_eq_endPos_iff, ← Pos.ofSliceFrom_inj]
@[simp]
theorem isEmpty_sliceFrom_eq_false_iff {s : Slice} {p : s.Pos} :
(s.sliceFrom p).isEmpty = false ↔ p ≠ s.endPos :=
Decidable.not_iff_not.1 (by simp)
@[simp]
theorem isEmpty_sliceTo {s : Slice} {p : s.Pos} :
(s.sliceTo p).isEmpty ↔ p = s.startPos := by
simp [← startPos_eq_endPos_iff, eq_comm (a := p), ← Pos.ofSliceTo_inj]
@[simp]
theorem isEmpty_sliceTo_eq_false_iff {s : Slice} {p : s.Pos} :
(s.sliceTo p).isEmpty = false ↔ p ≠ s.startPos :=
Decidable.not_iff_not.1 (by simp)
end Slice
theorem isEmpty_eq_utf8ByteSize_beq_zero {s : String} : s.isEmpty = (s.utf8ByteSize == 0) :=
(rfl)
theorem isEmpty_iff_utf8ByteSize_eq_zero {s : String} : s.isEmpty ↔ s.utf8ByteSize = 0 := by
simp [isEmpty_eq_utf8ByteSize_beq_zero]
@[simp]
theorem isEmpty_iff {s : String} : s.isEmpty ↔ s = "" := by
simp [isEmpty_iff_utf8ByteSize_eq_zero]
theorem startPos_ne_endPos_iff {s : String} : s.startPos ≠ s.endPos ↔ s ≠ "" := by
simp
theorem startPos_ne_endPos {s : String} : s ≠ "" → s.startPos ≠ s.endPos :=
startPos_ne_endPos_iff.2
@[simp]
theorem isEmpty_toSlice {s : String} : s.toSlice.isEmpty = s.isEmpty := by
simp [isEmpty_eq_utf8ByteSize_beq_zero, Slice.isEmpty_eq]
theorem isEmpty_toSlice_iff {s : String} : s.toSlice.isEmpty ↔ s = "" := by
simp
theorem eq_empty_iff_forall_eq {s : String} : s = "" ↔ ∀ (p q : s.Pos), p = q := by
rw [← isEmpty_toSlice_iff, Slice.isEmpty_iff_forall_eq]
exact ⟨fun h p q => by simpa [Pos.toSlice_inj] using h p.toSlice q.toSlice,
fun h p q => by simpa [Pos.ofToSlice_inj] using h (Pos.ofToSlice p) (Pos.ofToSlice q)⟩
theorem ne_empty_of_lt {s : String} {p q : s.Pos} :
p < q → s ≠ "" := by
rw [← Pos.toSlice_lt_toSlice_iff, ne_eq, ← isEmpty_toSlice_iff, Bool.not_eq_true]
exact Slice.isEmpty_eq_false_of_lt
@[simp]
theorem isEmpty_sliceFrom {s : String} {p : s.Pos} :
(s.sliceFrom p).isEmpty ↔ p = s.endPos := by
simp [← Slice.startPos_eq_endPos_iff, ← Pos.ofSliceFrom_inj]
@[simp]
theorem isEmpty_sliceFrom_eq_false_iff {s : String} {p : s.Pos} :
(s.sliceFrom p).isEmpty = false ↔ p ≠ s.endPos :=
Decidable.not_iff_not.1 (by simp)
@[simp]
theorem isEmpty_sliceTo {s : String} {p : s.Pos} :
(s.sliceTo p).isEmpty ↔ p = s.startPos := by
simp [← Slice.startPos_eq_endPos_iff, eq_comm (a := p), ← Pos.ofSliceTo_inj]
@[simp]
theorem isEmpty_sliceTo_eq_false_iff {s : String} {p : s.Pos} :
(s.sliceTo p).isEmpty = false ↔ p ≠ s.startPos :=
Decidable.not_iff_not.1 (by simp)
end String

12
src/Init/Data/String/Lemmas/Order.lean
View file

@ -39,6 +39,10 @@ theorem Slice.Pos.startPos_lt_iff {s : Slice} (p : s.Pos) : s.startPos < p ↔ p
theorem Slice.Pos.endPos_le {s : Slice} (p : s.Pos) : s.endPos ≤ p ↔ p = s.endPos :=
⟨fun h => Std.le_antisymm (le_endPos _) h, by simp +contextual⟩
@[simp]
theorem Slice.Pos.lt_endPos_iff {s : Slice} (p : s.Pos) : p < s.endPos ↔ p ≠ s.endPos := by
simp [← endPos_le, Std.not_le]
@[simp]
theorem Pos.le_startPos {s : String} (p : s.Pos) : p ≤ s.startPos ↔ p = s.startPos :=
⟨fun h => Std.le_antisymm h (startPos_le _), by simp +contextual⟩
@ -68,6 +72,14 @@ theorem Slice.Pos.ofSliceFrom_le_ofSliceFrom_iff {s : Slice} {p : s.Pos}
{q r : (s.sliceFrom p).Pos} : Slice.Pos.ofSliceFrom q ≤ Slice.Pos.ofSliceFrom r ↔ q ≤ r := by
simp [Slice.Pos.le_iff, Pos.Raw.le_iff]
theorem Slice.Pos.ofSliceTo_lt_ofSliceTo_iff {s : Slice} {p : s.Pos}
{q r : (s.sliceTo p).Pos} : Slice.Pos.ofSliceTo q < Slice.Pos.ofSliceTo r ↔ q < r := by
simp [Slice.Pos.lt_iff, Pos.Raw.lt_iff]
theorem Slice.Pos.ofSliceTo_le_ofSliceTo_iff {s : Slice} {p : s.Pos}
{q r : (s.sliceTo p).Pos} : Slice.Pos.ofSliceTo q ≤ Slice.Pos.ofSliceTo r ↔ q ≤ r := by
simp [Slice.Pos.le_iff, Pos.Raw.le_iff]
@[simp]
theorem Slice.Pos.offset_le_rawEndPos {s : Slice} {p : s.Pos} :
p.offset ≤ s.rawEndPos :=

400
src/Init/Data/String/Pattern/Basic.lean
View file

@ -1,7 +1,7 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
Authors: Henrik Böving, Markus Himmel
-/
module
@ -9,6 +9,10 @@ prelude
public import Init.Data.String.Basic
public import Init.Data.Iterators.Basic
public import Init.Data.Iterators.Consumers.Loop
import Init.Data.String.Lemmas.IsEmpty
import Init.Data.String.Termination
import Init.Data.String.OrderInstances
import Init.Data.String.Lemmas.Order
set_option doc.verso true
@ -41,9 +45,118 @@ inductive SearchStep (s : Slice) where
| matched (startPos endPos : s.Pos)
deriving Inhabited, BEq
namespace SearchStep
/-- The start position of a {name}`SearchStep`. -/
@[inline]
def startPos {s : Slice} (st : SearchStep s) : s.Pos :=
match st with
| .rejected startPos _ => startPos
| .matched startPos _ => startPos
@[simp]
theorem startPos_rejected {s : Slice} {p q : s.Pos} : (SearchStep.rejected p q).startPos = p := (rfl)
@[simp]
theorem startPos_matched {s : Slice} {p q : s.Pos} : (SearchStep.matched p q).startPos = p := (rfl)
/-- The end position of a {name}`SearchStep`. -/
@[inline]
def endPos {s : Slice} (st : SearchStep s) : s.Pos :=
match st with
| .rejected _ endPos => endPos
| .matched _ endPos => endPos
@[simp]
theorem endPos_rejected {s : Slice} {p q : s.Pos} : (SearchStep.rejected p q).endPos = q := (rfl)
@[simp]
theorem endPos_matched {s : Slice} {p q : s.Pos} : (SearchStep.matched p q).endPos = q := (rfl)
/--
Converts a {lean}`SearchStep (s.sliceFrom p)` into a {lean}`SearchStep s` by applying
{name}`Slice.Pos.ofSliceFrom` to the start and end position.
-/
def ofSliceFrom {s : Slice} {p : s.Pos} (st : SearchStep (s.sliceFrom p)) : SearchStep s :=
match st with
| .rejected l r => .rejected (Slice.Pos.ofSliceFrom l) (Slice.Pos.ofSliceFrom r)
| .matched l r => .matched (Slice.Pos.ofSliceFrom l) (Slice.Pos.ofSliceFrom r)
@[simp]
theorem startPos_ofSliceFrom {s : Slice} {p : s.Pos} {st : SearchStep (s.sliceFrom p)} :
st.ofSliceFrom.startPos = Slice.Pos.ofSliceFrom st.startPos := by
cases st <;> simp [ofSliceFrom]
@[simp]
theorem endPos_ofSliceFrom {s : Slice} {p : s.Pos} {st : SearchStep (s.sliceFrom p)} :
st.ofSliceFrom.endPos = Slice.Pos.ofSliceFrom st.endPos := by
cases st <;> simp [ofSliceFrom]
end SearchStep
/--
Provides simple pattern matching capabilities from the start of a {name}`Slice`.
-/
class ForwardPattern {ρ : Type} (pat : ρ) where
/--
Checks whether the slice starts with the pattern. If it does, the slice is returned with the
prefix removed; otherwise the result is {name}`none`.
-/
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 {name}`none`.
-/
dropPrefixOfNonempty? : (s : Slice) → (h : s.isEmpty = false) → Option s.Pos := fun s _ => dropPrefix? s
/--
Checks whether the slice starts with the pattern.
-/
startsWith : (s : Slice) → Bool := fun s => (dropPrefix? s).isSome
/--
A lawful forward pattern is one where the three functions {name}`ForwardPattern.dropPrefix?`,
{name}`ForwardPattern.dropPrefixOfNonempty?` and {name}`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 {lit}`LawfulForwardPatternModel` that asserts that the
{name}`ForwardPattern.dropPrefix?` function behaves like a function that drops the longest prefix
according to some notion of matching.
-/
class LawfulForwardPattern {ρ : Type} (pat : ρ) [ForwardPattern pat] : Prop where
dropPrefixOfNonempty?_eq {s : Slice} (h) :
ForwardPattern.dropPrefixOfNonempty? pat s h = ForwardPattern.dropPrefix? pat s
startsWith_eq (s : Slice) :
ForwardPattern.startsWith pat s = (ForwardPattern.dropPrefix? pat s).isSome
/--
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.
-/
class StrictForwardPattern {ρ : Type} (pat : ρ) [ForwardPattern pat] : Prop where
ne_startPos {s : Slice} (h) (q) :
ForwardPattern.dropPrefixOfNonempty? pat s h = some q → q ≠ s.startPos
/--
Provides a conversion from a pattern to an iterator of {name}`SearchStep` that searches for matches
of the pattern from the start towards the end of a {name}`Slice`.
While these operations can be implemented on top of {name}`ForwardPattern`, some patterns allow
for more efficient implementations. For example, a searcher for {name}`String` patterns derived
from the {name}`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
{module -checked}`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
{name (scope := "Init.Data.String.Pattern.Basic")}`ToForwardSearcher.defaultImplementation` can be
used to automatically derive an instance.
-/
class ToForwardSearcher {ρ : Type} (pat : ρ) (σ : outParam (Slice → Type)) where
/--
@ -53,25 +166,87 @@ class ToForwardSearcher {ρ : Type} (pat : ρ) (σ : outParam (Slice → Type))
-/
toSearcher : (s : Slice) → Std.Iter (α := σ s) (SearchStep s)
/--
Provides simple pattern matching capabilities from the start of a {name}`Slice`.
namespace ToForwardSearcher
While these operations can be implemented on top of {name}`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
{name (scope := "Init.Data.String.Pattern.Basic")}`ForwardPattern.defaultImplementation` can be used
to automatically derive an instance.
structure DefaultForwardSearcher {ρ : Type} (pat : ρ) (s : Slice) where
currPos : s.Pos
deriving Inhabited
namespace DefaultForwardSearcher
variable {ρ : Type} (pat : ρ)
@[inline]
def iter (s : Slice) : Std.Iter (α := DefaultForwardSearcher pat s) (SearchStep s) :=
⟨⟨s.startPos⟩⟩
instance (s : Slice) [ForwardPattern pat] :
Std.Iterator (DefaultForwardSearcher pat s) Id (SearchStep s) where
IsPlausibleStep it
| .yield it' (.rejected p₁ p₂) => ∃ (h : it.internalState.currPos ≠ s.endPos),
ForwardPattern.dropPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) = none ∧
p₁ = it.internalState.currPos ∧ p₂ = it.internalState.currPos.next h ∧
it'.internalState.currPos = it.internalState.currPos.next h
| .yield it' (.matched p₁ p₂) => ∃ (h : it.internalState.currPos ≠ s.endPos), ∃ pos,
ForwardPattern.dropPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) = some pos ∧
p₁ = it.internalState.currPos ∧ p₂ = Slice.Pos.ofSliceFrom pos ∧
it'.internalState.currPos = Slice.Pos.ofSliceFrom pos
| .done => it.internalState.currPos = s.endPos
| .skip _ => False
step it :=
if h : it.internalState.currPos = s.endPos then
pure (.deflate ⟨.done, by simp [h]⟩)
else
match h' : ForwardPattern.dropPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) with
| some pos =>
pure (.deflate ⟨.yield ⟨⟨Slice.Pos.ofSliceFrom pos⟩⟩
(.matched it.internalState.currPos (Slice.Pos.ofSliceFrom pos)), by simp [h, h']⟩)
| none =>
pure (.deflate ⟨.yield ⟨⟨it.internalState.currPos.next h⟩⟩
(.rejected it.internalState.currPos (it.internalState.currPos.next h)), by simp [h, h']⟩)
private def finitenessRelation (s : Slice) [ForwardPattern pat] [StrictForwardPattern pat] :
Std.Iterators.FinitenessRelation (DefaultForwardSearcher pat s) Id where
Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
wf := InvImage.wf _ WellFoundedRelation.wf
subrelation {it it'} h := by
simp_wf
obtain ⟨step, h, h'⟩ := h
match step with
| .yield it'' (.rejected p₁ p₂) =>
obtain ⟨_, ⟨-, -, -, h'⟩⟩ := h'
cases h
simp [h']
| .yield it'' (.matched p₁ p₂) =>
obtain ⟨_, pos, ⟨h₀, -, -, h'⟩⟩ := h'
cases h
have := StrictForwardPattern.ne_startPos _ _ h₀
rw [h']
exact Std.lt_of_le_of_lt Slice.Pos.le_ofSliceFrom
(Slice.Pos.ofSliceFrom_lt_ofSliceFrom_iff.2 ((Slice.Pos.startPos_lt_iff _).2 this))
instance {s : Slice} [ForwardPattern pat] [StrictForwardPattern pat] :
Std.Iterators.Finite (DefaultForwardSearcher pat s) Id :=
.of_finitenessRelation (finitenessRelation pat s)
instance [ForwardPattern pat] : Std.IteratorLoop (DefaultForwardSearcher pat s) Id Id :=
.defaultImplementation
end DefaultForwardSearcher
/--
The default implementation of {name}`ToForwardSearcher` repeatedly tries to match the pattern using
the given {name}`ForwardPattern` instance.
It is sometimes possible to give a more efficient implementation; see {name}`ToForwardSearcher`
for more details.
-/
class ForwardPattern {ρ : Type} (pat : ρ) where
/--
Checks whether the slice starts with the pattern.
-/
startsWith : Slice → Bool
/--
Checks whether the slice starts with the pattern. If it does, the slice is returned with the
prefix removed; otherwise the result is {name}`none`.
-/
dropPrefix? : (s : Slice) → Option s.Pos
@[inline]
def defaultImplementation [ForwardPattern pat] :
ToForwardSearcher pat (DefaultForwardSearcher pat) where
toSearcher := DefaultForwardSearcher.iter pat
end ToForwardSearcher
namespace Internal
@ -123,37 +298,69 @@ def memcmpSlice (lhs rhs : Slice) (lstart : String.Pos.Raw) (rstart : String.Pos
end Internal
namespace ForwardPattern
/--
Provides simple pattern matching capabilities from the end of a {name}`Slice`.
-/
class BackwardPattern {ρ : Type} (pat : ρ) where
/--
Checks whether the slice ends with the pattern. If it does, the slice is returned with the
suffix removed; otherwise the result is {name}`none`.
-/
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 {name}`none`.
-/
dropSuffixOfNonempty? : (s : Slice) → (h : s.isEmpty = false) → Option s.Pos := fun s _ => dropSuffix? s
/--
Checks whether the slice ends with the pattern.
-/
endsWith : Slice → Bool := fun s => (dropSuffix? s).isSome
variable {ρ : Type} {σ : Slice → Type}
variable [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
variable (pat : ρ) [ToForwardSearcher pat σ]
/--
A lawful backward pattern is one where the three functions {name}`BackwardPattern.dropSuffix?`,
{name}`BackwardPattern.dropSuffixOfNonempty?` and {name}`BackwardPattern.endsWith` agree for any
given input slice.
@[specialize pat]
def defaultStartsWith (s : Slice) [Std.IteratorLoop (σ s) Id Id] : Bool :=
let searcher := ToForwardSearcher.toSearcher pat s
match searcher.first? with
| some (.matched start ..) => s.startPos = start
| _ => false
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.
@[specialize pat]
def defaultDropPrefix? (s : Slice) [Std.IteratorLoop (σ s) Id Id] : Option s.Pos :=
let searcher := ToForwardSearcher.toSearcher pat s
match searcher.first? with
| some (.matched _ endPos) => some endPos
| _ => none
There is a stronger lawfulness typeclass {lit}`LawfulBackwardPatternModel` that asserts that the
{name}`BackwardPattern.dropSuffix?` function behaves like a function that drops the longest prefix
according to some notion of matching.
-/
class LawfulBackwardPattern {ρ : Type} (pat : ρ) [BackwardPattern pat] : Prop where
dropSuffixOfNonempty?_eq {s : Slice} (h) :
BackwardPattern.dropSuffixOfNonempty? pat s h = BackwardPattern.dropSuffix? pat s
endsWith_eq (s : Slice) :
BackwardPattern.endsWith pat s = (BackwardPattern.dropSuffix? pat s).isSome
@[always_inline, inline]
def defaultImplementation {pat : ρ} [ToForwardSearcher pat σ] [∀ s, Std.IteratorLoop (σ s) Id Id] :
ForwardPattern pat where
startsWith s := defaultStartsWith pat s
dropPrefix? s := defaultDropPrefix? pat s
/--
A strict backward pattern is one which never drops an empty suffix.
end ForwardPattern
This condition ensures that the default searcher derived from the backward pattern is a finite
iterator.
-/
class StrictBackwardPattern {ρ : Type} (pat : ρ) [BackwardPattern pat] : Prop where
ne_endPos {s : Slice} (h) (q) :
BackwardPattern.dropSuffixOfNonempty? pat s h = some q → q ≠ s.endPos
/--
Provides a conversion from a pattern to an iterator of {name}`SearchStep` searching for matches of
the pattern from the end towards the start of a {name}`Slice`.
While these operations can be implemented on top of {name}`BackwardPattern`, some patterns allow
for more efficient implementations. For example, a searcher for {name}`String` patterns derived
from the {name}`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
{module -checked}`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
{name (scope := "Init.Data.String.Pattern.Basic")}`ToBackwardSearcher.defaultImplementation` can be
used to automatically derive an instance.
-/
class ToBackwardSearcher {ρ : Type} (pat : ρ) (σ : outParam (Slice → Type)) where
/--
@ -163,51 +370,84 @@ class ToBackwardSearcher {ρ : Type} (pat : ρ) (σ : outParam (Slice → Type))
-/
toSearcher : (s : Slice) → Std.Iter (α := σ s) (SearchStep s)
/--
Provides simple pattern matching capabilities from the end of a {name}`Slice`.
While these operations can be implemented on top of {name}`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
{name (scope := "Init.Data.String.Pattern.Basic")}`BackwardPattern.defaultImplementation` can be
used to automatically derive an instance.
-/
class BackwardPattern {ρ : Type} (pat : ρ) where
/--
Checks whether the slice ends with the pattern.
-/
endsWith : Slice → Bool
/--
Checks whether the slice ends with the pattern. If it does, the slice is returned with the
suffix removed; otherwise the result is {name}`none`.
-/
dropSuffix? : (s : Slice) → Option s.Pos
namespace ToBackwardSearcher
variable {ρ : Type} {σ : Slice → Type}
variable [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
variable (pat : ρ) [ToBackwardSearcher pat σ]
structure DefaultBackwardSearcher {ρ : Type} (pat : ρ) (s : Slice) where
currPos : s.Pos
deriving Inhabited
@[specialize pat]
def defaultEndsWith (s : Slice) [Std.IteratorLoop (σ s) Id Id] : Bool :=
let searcher := ToBackwardSearcher.toSearcher pat s
match searcher.first? with
| some (.matched _ endPos) => s.endPos = endPos
| _ => false
namespace DefaultBackwardSearcher
@[specialize pat]
def defaultDropSuffix? (s : Slice) [Std.IteratorLoop (σ s) Id Id] : Option s.Pos :=
let searcher := ToBackwardSearcher.toSearcher pat s
match searcher.first? with
| some (.matched startPos _) => some startPos
| _ => none
variable {ρ : Type} (pat : ρ)
@[always_inline, inline]
def defaultImplementation {pat : ρ} [ToBackwardSearcher pat σ] [∀ s, Std.IteratorLoop (σ s) Id Id] :
BackwardPattern pat where
endsWith s := defaultEndsWith pat s
dropSuffix? s := defaultDropSuffix? pat s
@[inline]
def iter (s : Slice) : Std.Iter (α := DefaultBackwardSearcher pat s) (SearchStep s) :=
⟨⟨s.endPos⟩⟩
instance (s : Slice) [BackwardPattern pat] :
Std.Iterator (DefaultBackwardSearcher pat s) Id (SearchStep s) where
IsPlausibleStep it
| .yield it' (.rejected p₁ p₂) => ∃ (h : it.internalState.currPos ≠ s.startPos),
BackwardPattern.dropSuffixOfNonempty? pat (s.sliceTo it.internalState.currPos) (by simpa) = none ∧
p₁ = it.internalState.currPos.prev h ∧ p₂ = it.internalState.currPos ∧
it'.internalState.currPos = it.internalState.currPos.prev h
| .yield it' (.matched p₁ p₂) => ∃ (h : it.internalState.currPos ≠ s.startPos), ∃ pos,
BackwardPattern.dropSuffixOfNonempty? pat (s.sliceTo it.internalState.currPos) (by simpa) = some pos ∧
p₁ = Slice.Pos.ofSliceTo pos ∧ p₂ = it.internalState.currPos ∧
it'.internalState.currPos = Slice.Pos.ofSliceTo pos
| .done => it.internalState.currPos = s.startPos
| .skip _ => False
step it :=
if h : it.internalState.currPos = s.startPos then
pure (.deflate ⟨.done, by simp [h]⟩)
else
match h' : BackwardPattern.dropSuffixOfNonempty? pat (s.sliceTo it.internalState.currPos) (by simpa) with
| some pos =>
pure (.deflate ⟨.yield ⟨⟨Slice.Pos.ofSliceTo pos⟩⟩
(.matched (Slice.Pos.ofSliceTo pos) it.internalState.currPos), by simp [h, h']⟩)
| none =>
pure (.deflate ⟨.yield ⟨⟨it.internalState.currPos.prev h⟩⟩
(.rejected (it.internalState.currPos.prev h) it.internalState.currPos), by simp [h, h']⟩)
private def finitenessRelation (s : Slice) [BackwardPattern pat] [StrictBackwardPattern pat] :
Std.Iterators.FinitenessRelation (DefaultBackwardSearcher pat s) Id where
Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos.down)
wf := InvImage.wf _ WellFoundedRelation.wf
subrelation {it it'} h := by
simp_wf
obtain ⟨step, h, h'⟩ := h
match step with
| .yield it'' (.rejected p₁ p₂) =>
obtain ⟨_, ⟨-, -, -, h'⟩⟩ := h'
cases h
simp [h']
| .yield it'' (.matched p₁ p₂) =>
obtain ⟨_, pos, ⟨h₀, -, -, h'⟩⟩ := h'
cases h
have := StrictBackwardPattern.ne_endPos _ _ h₀
rw [h']
exact Std.lt_of_lt_of_le (Slice.Pos.ofSliceTo_lt_ofSliceTo_iff.2 ((Slice.Pos.lt_endPos_iff _).2 this)) Slice.Pos.ofSliceTo_le
instance {s : Slice} [BackwardPattern pat] [StrictBackwardPattern pat] :
Std.Iterators.Finite (DefaultBackwardSearcher pat s) Id :=
.of_finitenessRelation (finitenessRelation pat s)
instance [BackwardPattern pat] : Std.IteratorLoop (DefaultBackwardSearcher pat s) Id Id :=
.defaultImplementation
end DefaultBackwardSearcher
/--
The default implementation of {name}`ToBackwardSearcher` repeatedly tries to match the pattern using
the given {name}`BackwardPattern` instance.
It is sometimes possible to give a more efficient implementation; see {name}`ToBackwardSearcher`
for more details.
-/
@[inline]
def defaultImplementation [BackwardPattern pat] :
ToBackwardSearcher pat (DefaultBackwardSearcher pat) where
toSearcher := DefaultBackwardSearcher.iter pat
end ToBackwardSearcher

182
src/Init/Data/String/Pattern/Char.lean
View file

@ -1,7 +1,7 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
Authors: Henrik Böving, Markus Himmel
-/
module
@ -9,6 +9,8 @@ prelude
public import Init.Data.String.Pattern.Basic
public import Init.Data.Iterators.Consumers.Monadic.Loop
import Init.Data.String.Termination
import Init.Data.String.Lemmas.IsEmpty
import Init.Data.String.Lemmas.Order
set_option doc.verso true
@ -20,132 +22,82 @@ public section
namespace String.Slice.Pattern
structure ForwardCharSearcher (needle : Char) (s : Slice) where
currPos : s.Pos
deriving Inhabited
namespace Char
namespace ForwardCharSearcher
@[inline]
def iter (c : Char) (s : Slice) : Std.Iter (α := ForwardCharSearcher c s) (SearchStep s) :=
{ internalState := { currPos := s.startPos }}
instance (s : Slice) : Std.Iterator (ForwardCharSearcher c s) Id (SearchStep s) where
IsPlausibleStep it
| .yield it' out =>
∃ h1 : it.internalState.currPos ≠ s.endPos,
it'.internalState.currPos = it.internalState.currPos.next h1 ∧
match out with
| .matched startPos endPos =>
it.internalState.currPos = startPos ∧
it'.internalState.currPos = endPos ∧
it.internalState.currPos.get h1 = c
| .rejected startPos endPos =>
it.internalState.currPos = startPos ∧
it'.internalState.currPos = endPos ∧
it.internalState.currPos.get h1 ≠ c
| .skip _ => False
| .done => it.internalState.currPos = s.endPos
step := fun ⟨⟨currPos⟩⟩ =>
if h1 : currPos = s.endPos then
pure (.deflate ⟨.done, by simp [h1]⟩)
instance {c : Char} : ForwardPattern c where
dropPrefixOfNonempty? s h :=
if s.startPos.get (by exact Slice.startPos_ne_endPos h) = c then
some (s.startPos.next (by exact Slice.startPos_ne_endPos h))
else
let nextPos := currPos.next h1
let nextIt := ⟨⟨nextPos⟩⟩
if h2 : currPos.get h1 = c then
pure (.deflate ⟨.yield nextIt (.matched currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩)
else
pure (.deflate ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩)
none
dropPrefix? s :=
if h : s.startPos = s.endPos then
none
else if s.startPos.get h = c then
some (s.startPos.next h)
else
none
startsWith s :=
if h : s.startPos = s.endPos then
false
else
s.startPos.get h = c
def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharSearcher s c) Id where
Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
wf := InvImage.wf _ WellFoundedRelation.wf
subrelation {it it'} h := by
simp_wf
obtain ⟨step, h, h'⟩ := h
cases step
· cases h
obtain ⟨_, h2, _⟩ := h'
simp [h2]
· cases h'
· cases h
instance {c : Char} : StrictForwardPattern c where
ne_startPos {s h q} := by
simp only [ForwardPattern.dropPrefixOfNonempty?, Option.ite_none_right_eq_some,
Option.some.injEq, ne_eq, and_imp]
rintro _ rfl
simp
instance : Std.Iterators.Finite (ForwardCharSearcher s c) Id :=
.of_finitenessRelation finitenessRelation
instance {c : Char} : LawfulForwardPattern c where
dropPrefixOfNonempty?_eq {s h} := by
simp [ForwardPattern.dropPrefixOfNonempty?, ForwardPattern.dropPrefix?,
Slice.startPos_eq_endPos_iff, h]
startsWith_eq {s} := by
simp only [ForwardPattern.startsWith, ForwardPattern.dropPrefix?]
split <;> (try split) <;> simp_all
instance : Std.IteratorLoop (ForwardCharSearcher s c) Id Id :=
instance {c : Char} : ToForwardSearcher c (ToForwardSearcher.DefaultForwardSearcher c) :=
.defaultImplementation
instance {c : Char} : ToForwardSearcher c (ForwardCharSearcher c) where
toSearcher := iter c
instance {c : Char} : ForwardPattern c := .defaultImplementation
end ForwardCharSearcher
structure BackwardCharSearcher (s : Slice) where
currPos : s.Pos
needle : Char
deriving Inhabited
namespace BackwardCharSearcher
@[inline]
def iter (c : Char) (s : Slice) : Std.Iter (α := BackwardCharSearcher s) (SearchStep s) :=
{ internalState := { currPos := s.endPos, needle := c }}
instance (s : Slice) : Std.Iterator (BackwardCharSearcher s) Id (SearchStep s) where
IsPlausibleStep it
| .yield it' out =>
it.internalState.needle = it'.internalState.needle ∧
∃ h1 : it.internalState.currPos ≠ s.startPos,
it'.internalState.currPos = it.internalState.currPos.prev h1 ∧
match out with
| .matched startPos endPos =>
it.internalState.currPos = endPos ∧
it'.internalState.currPos = startPos ∧
(it.internalState.currPos.prev h1).get Pos.prev_ne_endPos = it.internalState.needle
| .rejected startPos endPos =>
it.internalState.currPos = endPos ∧
it'.internalState.currPos = startPos ∧
(it.internalState.currPos.prev h1).get Pos.prev_ne_endPos ≠ it.internalState.needle
| .skip _ => False
| .done => it.internalState.currPos = s.startPos
step := fun ⟨currPos, needle⟩ =>
if h1 : currPos = s.startPos then
pure (.deflate ⟨.done, by simp [h1]⟩)
instance {c : Char} : BackwardPattern c where
dropSuffixOfNonempty? s h :=
if (s.endPos.prev (Ne.symm (by exact Slice.startPos_ne_endPos h))).get (by simp) = c then
some (s.endPos.prev (Ne.symm (by exact Slice.startPos_ne_endPos h)))
else
let nextPos := currPos.prev h1
let nextIt := ⟨nextPos, needle⟩
if h2 : nextPos.get Pos.prev_ne_endPos = needle then
pure (.deflate ⟨.yield nextIt (.matched nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩)
else
pure (.deflate ⟨.yield nextIt (.rejected nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩)
none
dropSuffix? s :=
if h : s.endPos = s.startPos then
none
else if (s.endPos.prev h).get (by simp) = c then
some (s.endPos.prev h)
else
none
endsWith s :=
if h : s.endPos = s.startPos then
false
else
(s.endPos.prev h).get (by simp) = c
def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharSearcher s) Id where
Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos.down)
wf := InvImage.wf _ WellFoundedRelation.wf
subrelation {it it'} h := by
simp_wf
obtain ⟨step, h, h'⟩ := h
cases step
· cases h
obtain ⟨_, h1, h2, _⟩ := h'
simp [h2]
· cases h'
· cases h
instance {c : Char} : StrictBackwardPattern c where
ne_endPos {s h q} := by
simp only [BackwardPattern.dropSuffixOfNonempty?, Option.ite_none_right_eq_some,
Option.some.injEq, ne_eq, and_imp]
rintro _ rfl
simp
instance : Std.Iterators.Finite (BackwardCharSearcher s) Id :=
.of_finitenessRelation finitenessRelation
instance {c : Char} : LawfulBackwardPattern c where
dropSuffixOfNonempty?_eq {s h} := by
simp [BackwardPattern.dropSuffixOfNonempty?, BackwardPattern.dropSuffix?,
Eq.comm (a := s.endPos), Slice.startPos_eq_endPos_iff, h]
endsWith_eq {s} := by
simp only [BackwardPattern.endsWith, BackwardPattern.dropSuffix?]
split <;> (try split) <;> simp_all
instance : Std.IteratorLoop (BackwardCharSearcher s) Id Id :=
instance {c : Char} : ToBackwardSearcher c (ToBackwardSearcher.DefaultBackwardSearcher c) :=
.defaultImplementation
instance {c : Char} : ToBackwardSearcher c BackwardCharSearcher where
toSearcher := iter c
instance {c : Char} : BackwardPattern c := ToBackwardSearcher.defaultImplementation
end BackwardCharSearcher
end Char
end String.Slice.Pattern

234
src/Init/Data/String/Pattern/Pred.lean
View file

@ -1,7 +1,7 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
Authors: Henrik Böving, Markus Himmel
-/
module
@ -9,6 +9,8 @@ prelude
public import Init.Data.String.Pattern.Basic
public import Init.Data.Iterators.Consumers.Monadic.Loop
import Init.Data.String.Termination
public import Init.Data.String.Lemmas.IsEmpty
import Init.Data.String.Lemmas.Order
set_option doc.verso true
@ -21,152 +23,116 @@ public section
namespace String.Slice.Pattern
structure ForwardCharPredSearcher (p : Char → Bool) (s : Slice) where
currPos : s.Pos
deriving Inhabited
namespace CharPred
namespace ForwardCharPredSearcher
@[inline]
def iter (p : Char → Bool) (s : Slice) : Std.Iter (α := ForwardCharPredSearcher p s) (SearchStep s) :=
{ internalState := { currPos := s.startPos }}
instance (s : Slice) : Std.Iterator (ForwardCharPredSearcher p s) Id (SearchStep s) where
IsPlausibleStep it
| .yield it' out =>
∃ h1 : it.internalState.currPos ≠ s.endPos,
it'.internalState.currPos = it.internalState.currPos.next h1 ∧
match out with
| .matched startPos endPos =>
it.internalState.currPos = startPos ∧
it'.internalState.currPos = endPos ∧
p (it.internalState.currPos.get h1)
| .rejected startPos endPos =>
it.internalState.currPos = startPos ∧
it'.internalState.currPos = endPos ∧
¬ p (it.internalState.currPos.get h1)
| .skip _ => False
| .done => it.internalState.currPos = s.endPos
step := fun ⟨⟨currPos⟩⟩ =>
if h1 : currPos = s.endPos then
pure (.deflate ⟨.done, by simp [h1]⟩)
@[default_instance]
instance {p : Char → Bool} : ForwardPattern p where
dropPrefixOfNonempty? s h :=
if p (s.startPos.get (Slice.startPos_ne_endPos h)) then
some (s.startPos.next (Slice.startPos_ne_endPos h))
else
let nextPos := currPos.next h1
let nextIt := ⟨⟨nextPos⟩⟩
if h2 : p <| currPos.get h1 then
pure (.deflate ⟨.yield nextIt (.matched currPos nextPos), by simp [h1, h2, nextPos, nextIt]⟩)
else
pure (.deflate ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextPos, nextIt]⟩)
def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharPredSearcher p s) Id where
Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
wf := InvImage.wf _ WellFoundedRelation.wf
subrelation {it it'} h := by
simp_wf
obtain ⟨step, h, h'⟩ := h
cases step
· cases h
obtain ⟨_, h2, _⟩ := h'
simp [h2]
· cases h'
· cases h
instance : Std.Iterators.Finite (ForwardCharPredSearcher p s) Id :=
.of_finitenessRelation finitenessRelation
instance : Std.IteratorLoop (ForwardCharPredSearcher p s) Id Id :=
.defaultImplementation
@[default_instance]
instance {p : Char → Bool} : ToForwardSearcher p (ForwardCharPredSearcher p) where
toSearcher := iter p
@[default_instance]
instance {p : Char → Bool} : ForwardPattern p := .defaultImplementation
instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ForwardCharPredSearcher p) where
toSearcher := iter (decide <| p ·)
instance {p : Char → Prop} [DecidablePred p] : ForwardPattern p :=
.defaultImplementation
end ForwardCharPredSearcher
structure BackwardCharPredSearcher (s : Slice) where
currPos : s.Pos
needle : Char → Bool
deriving Inhabited
namespace BackwardCharPredSearcher
@[inline]
def iter (c : Char → Bool) (s : Slice) : Std.Iter (α := BackwardCharPredSearcher s) (SearchStep s) :=
{ internalState := { currPos := s.endPos, needle := c }}
instance (s : Slice) : Std.Iterator (BackwardCharPredSearcher s) Id (SearchStep s) where
IsPlausibleStep it
| .yield it' out =>
it.internalState.needle = it'.internalState.needle ∧
∃ h1 : it.internalState.currPos ≠ s.startPos,
it'.internalState.currPos = it.internalState.currPos.prev h1 ∧
match out with
| .matched startPos endPos =>
it.internalState.currPos = endPos ∧
it'.internalState.currPos = startPos ∧
it.internalState.needle ((it.internalState.currPos.prev h1).get Pos.prev_ne_endPos)
| .rejected startPos endPos =>
it.internalState.currPos = endPos ∧
it'.internalState.currPos = startPos ∧
¬ it.internalState.needle ((it.internalState.currPos.prev h1).get Pos.prev_ne_endPos)
| .skip _ => False
| .done => it.internalState.currPos = s.startPos
step := fun ⟨currPos, needle⟩ =>
if h1 : currPos = s.startPos then
pure (.deflate ⟨.done, by simp [h1]⟩)
none
dropPrefix? s :=
if h : s.startPos = s.endPos then
none
else if p (s.startPos.get h) then
some (s.startPos.next h)
else
let nextPos := currPos.prev h1
let nextIt := ⟨nextPos, needle⟩
if h2 : needle <| nextPos.get Pos.prev_ne_endPos then
pure (.deflate ⟨.yield nextIt (.matched nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩)
else
pure (.deflate ⟨.yield nextIt (.rejected nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩)
none
startsWith s :=
if h : s.startPos = s.endPos then
false
else
p (s.startPos.get h)
def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharPredSearcher s) Id where
Rel := InvImage WellFoundedRelation.rel
(fun it => it.internalState.currPos.offset.byteIdx)
wf := InvImage.wf _ WellFoundedRelation.wf
subrelation {it it'} h := by
simp_wf
obtain ⟨step, h, h'⟩ := h
cases step
· cases h
obtain ⟨_, h1, h2, _⟩ := h'
have h3 := Pos.offset_prev_lt_offset (h := h1)
simp [Pos.ext_iff, String.Pos.Raw.ext_iff, String.Pos.Raw.lt_iff] at h2 h3
omega
· cases h'
· cases h
instance {p : Char → Bool} : StrictForwardPattern p where
ne_startPos {s h q} := by
simp only [ForwardPattern.dropPrefixOfNonempty?, Option.ite_none_right_eq_some,
Option.some.injEq, ne_eq, and_imp]
rintro _ rfl
simp
instance : Std.Iterators.Finite (BackwardCharPredSearcher s) Id :=
.of_finitenessRelation finitenessRelation
instance {p : Char → Bool} : LawfulForwardPattern p where
dropPrefixOfNonempty?_eq {s} h := by
simp [ForwardPattern.dropPrefixOfNonempty?, ForwardPattern.dropPrefix?,
Slice.startPos_eq_endPos_iff, h]
startsWith_eq s := by
simp only [ForwardPattern.startsWith, ForwardPattern.dropPrefix?]
split <;> (try split) <;> simp_all
instance : Std.IteratorLoop (BackwardCharPredSearcher s) Id Id :=
@[default_instance]
instance {p : Char → Bool} : ToForwardSearcher p (ToForwardSearcher.DefaultForwardSearcher p) :=
.defaultImplementation
instance {p : Char → Prop} [DecidablePred p] : ForwardPattern p where
dropPrefixOfNonempty? s h := ForwardPattern.dropPrefixOfNonempty? (decide <| p ·) s h
dropPrefix? s := ForwardPattern.dropPrefix? (decide <| p ·) s
startsWith s := ForwardPattern.startsWith (decide <| p ·) s
instance {p : Char → Prop} [DecidablePred p] : StrictForwardPattern p where
ne_startPos h q := StrictForwardPattern.ne_startPos (pat := (decide <| p ·)) h q
instance {p : Char → Prop} [DecidablePred p] : LawfulForwardPattern p where
dropPrefixOfNonempty?_eq h := LawfulForwardPattern.dropPrefixOfNonempty?_eq (pat := (decide <| p ·)) h
startsWith_eq s := LawfulForwardPattern.startsWith_eq (pat := (decide <| p ·)) s
instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ToForwardSearcher.DefaultForwardSearcher p) :=
.defaultImplementation
@[default_instance]
instance {p : Char → Bool} : ToBackwardSearcher p BackwardCharPredSearcher where
toSearcher := iter p
instance {p : Char → Bool} : BackwardPattern p where
dropSuffixOfNonempty? s h :=
if p ((s.endPos.prev (Ne.symm (by exact Slice.startPos_ne_endPos h))).get (by simp)) then
some (s.endPos.prev (Ne.symm (by exact Slice.startPos_ne_endPos h)))
else
none
dropSuffix? s :=
if h : s.endPos = s.startPos then
none
else if p ((s.endPos.prev h).get (by simp)) then
some (s.endPos.prev h)
else
none
endsWith s :=
if h : s.endPos = s.startPos then
false
else
p ((s.endPos.prev h).get (by simp))
instance {p : Char → Bool} : StrictBackwardPattern p where
ne_endPos {s h q} := by
simp only [BackwardPattern.dropSuffixOfNonempty?, Option.ite_none_right_eq_some,
Option.some.injEq, ne_eq, and_imp]
rintro _ rfl
simp
instance {p : Char → Bool} : LawfulBackwardPattern p where
dropSuffixOfNonempty?_eq {s h} := by
simp [BackwardPattern.dropSuffixOfNonempty?, BackwardPattern.dropSuffix?,
Eq.comm (a := s.endPos), Slice.startPos_eq_endPos_iff, h]
endsWith_eq {s} := by
simp only [BackwardPattern.endsWith, BackwardPattern.dropSuffix?]
split <;> (try split) <;> simp_all
@[default_instance]
instance {p : Char → Bool} : BackwardPattern p := ToBackwardSearcher.defaultImplementation
instance {p : Char → Bool} : ToBackwardSearcher p (ToBackwardSearcher.DefaultBackwardSearcher p) :=
.defaultImplementation
instance {p : Char → Prop} [DecidablePred p] : ToBackwardSearcher p BackwardCharPredSearcher where
toSearcher := iter (decide <| p ·)
instance {p : Char → Prop} [DecidablePred p] : BackwardPattern p where
dropSuffixOfNonempty? s h := BackwardPattern.dropSuffixOfNonempty? (decide <| p ·) s h
dropSuffix? s := BackwardPattern.dropSuffix? (decide <| p ·) s
endsWith s := BackwardPattern.endsWith (decide <| p ·) s
instance {p : Char → Prop} [DecidablePred p] : BackwardPattern p :=
ToBackwardSearcher.defaultImplementation
instance {p : Char → Prop} [DecidablePred p] : StrictBackwardPattern p where
ne_endPos h q := StrictBackwardPattern.ne_endPos (pat := (decide <| p ·)) h q
end BackwardCharPredSearcher
instance {p : Char → Prop} [DecidablePred p] : LawfulBackwardPattern p where
dropSuffixOfNonempty?_eq h := LawfulBackwardPattern.dropSuffixOfNonempty?_eq (pat := (decide <| p ·)) h
endsWith_eq s := LawfulBackwardPattern.endsWith_eq (pat := (decide <| p ·)) s
instance {p : Char → Prop} [DecidablePred p] : ToBackwardSearcher p (ToBackwardSearcher.DefaultBackwardSearcher p) :=
.defaultImplementation
end CharPred
end String.Slice.Pattern

12
src/Init/Data/String/Slice.lean
View file

@ -46,18 +46,6 @@ instance : HAppend String String.Slice String where
open Pattern
/--
Checks whether a slice is empty.
Empty slices have {name}`utf8ByteSize` {lean}`0`.
Examples:
* {lean}`"".toSlice.isEmpty = true`
* {lean}`" ".toSlice.isEmpty = false`
-/
@[inline]
def isEmpty (s : Slice) : Bool := s.utf8ByteSize == 0
/--
Checks whether {name}`s1` and {name}`s2` represent the same string, even if they are slices of
different base strings or different slices within the same string.