feat: split and splitInclusive iterators are finite (#10820)
This PR shows that the iterators returned by `String.Slice.split` and `String.Slice.splitInclusive` are finite as long as the forward matcher iterator for the pattern is finite (which we already know for all of our patterns). At actually also completely redefines the iterators to avoid the inner loop in `Internal.nextMatch` which generates inefficient code. Instead, when encountering a mismach from the matcher, we `skip` the split iterator.
This commit is contained in:
Markus Himmel
GitHub
parent
71f1a6c164
commit
c981ebc546
5 changed files with 248 additions and 139 deletions
|
|
@ -241,6 +241,16 @@ def IterStep.successor : IterStep α β → Option α
|
|||
| .skip it => some it
|
||||
| .done => none
|
||||
|
||||
@[simp]
|
||||
theorem IterStep.successor_yield {it : α} {out : β} :
|
||||
(IterStep.yield it out).successor = some it := rfl
|
||||
|
||||
@[simp]
|
||||
theorem IterStep.successor_skip {it : α} : (IterStep.skip (β := β) it).successor = some it := rfl
|
||||
|
||||
@[simp]
|
||||
theorem IterStep.successor_done : (IterStep.done (α := α) (β := β)).successor = none := rfl
|
||||
|
||||
/--
|
||||
If present, applies `f` to the iterator of an `IterStep` and replaces the iterator
|
||||
with the result of the application of `f`.
|
||||
|
|
@ -543,6 +553,10 @@ def Iter.IsPlausibleSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β]
|
|||
(it' it : Iter (α := α) β) : Prop :=
|
||||
it'.toIterM.IsPlausibleSuccessorOf it.toIterM
|
||||
|
||||
theorem Iter.isPlausibleSuccessorOf_eq_invImage {α : Type w} {β : Type w} [Iterator α Id β] :
|
||||
IsPlausibleSuccessorOf (α := α) (β := β) =
|
||||
InvImage (IterM.IsPlausibleSuccessorOf (α := α) (β := β) (m := Id)) Iter.toIterM := rfl
|
||||
|
||||
theorem Iter.isPlausibleSuccessorOf_iff_exists {α : Type w} {β : Type w} [Iterator α Id β]
|
||||
{it' it : Iter (α := α) β} :
|
||||
it'.IsPlausibleSuccessorOf it ↔ ∃ step, step.successor = some it' ∧ it.IsPlausibleStep step := by
|
||||
|
|
@ -555,6 +569,16 @@ theorem Iter.isPlausibleSuccessorOf_iff_exists {α : Type w} {β : Type w} [Iter
|
|||
exact ⟨step.mapIterator Iter.toIterM,
|
||||
by cases step <;> simp_all [IterStep.successor, Iter.IsPlausibleStep]⟩
|
||||
|
||||
theorem Iter.IsPlausibleStep.isPlausibleSuccessor_of_yield {α : Type w} {β : Type w}
|
||||
[Iterator α Id β] {it' it : Iter (α := α) β} {out : β}
|
||||
(h : it.IsPlausibleStep (.yield it' out)) : it'.IsPlausibleSuccessorOf it := by
|
||||
simpa [isPlausibleSuccessorOf_iff_exists] using ⟨.yield it' out, by simp [h]⟩
|
||||
|
||||
theorem Iter.IsPlausibleStep.isPlausibleSuccessor_of_skip {α : Type w} {β : Type w}
|
||||
[Iterator α Id β] {it' it : Iter (α := α) β} (h : it.IsPlausibleStep (.skip it')) :
|
||||
it'.IsPlausibleSuccessorOf it := by
|
||||
simpa [isPlausibleSuccessorOf_iff_exists] using ⟨.skip it', by simp [h]⟩
|
||||
|
||||
/--
|
||||
Asserts that a certain iterator `it` could plausibly yield the value `out` after an arbitrary
|
||||
number of steps.
|
||||
|
|
@ -656,6 +680,10 @@ Given this typeclass, termination proofs for well-founded recursion over an iter
|
|||
class Finite (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Prop where
|
||||
wf : WellFounded (IterM.IsPlausibleSuccessorOf (α := α) (m := m))
|
||||
|
||||
theorem Finite.wf_of_id {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] :
|
||||
WellFounded (Iter.IsPlausibleSuccessorOf (α := α)) := by
|
||||
simpa [Iter.isPlausibleSuccessorOf_eq_invImage] using InvImage.wf _ Finite.wf
|
||||
|
||||
/--
|
||||
This type is a wrapper around `IterM` so that it becomes a useful termination measure for
|
||||
recursion over finite iterators. See also `IterM.finitelyManySteps` and `Iter.finitelyManySteps`.
|
||||
|
|
@ -705,6 +733,12 @@ theorem IterM.TerminationMeasures.Finite.rel_of_skip
|
|||
Rel ⟨it'⟩ ⟨it⟩ := by
|
||||
exact .single ⟨_, rfl, h⟩
|
||||
|
||||
theorem IterM.TerminationMeasures.Finite.rel_trans
|
||||
{α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
|
||||
{it it' it'' : TerminationMeasures.Finite α m} :
|
||||
it.Rel it' → it'.Rel it'' → it.Rel it'' :=
|
||||
.trans
|
||||
|
||||
macro_rules | `(tactic| decreasing_trivial) => `(tactic|
|
||||
first
|
||||
| exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
|
||||
|
|
|
|||
|
|
@ -94,7 +94,7 @@ it.filterMapWithPostcondition ---a'-----c'-------⊥
|
|||
**Termination properties:**
|
||||
|
||||
* `Finite` instance: only if `it` is finite
|
||||
* `Productive` instance: only if `it` is finite`
|
||||
* `Productive` instance: only if `it` is finite
|
||||
|
||||
For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
|
||||
no `Finite` (or `Productive`) instance is provided. For example, if `f` never returns `none`, then
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ inductive SearchStep (s : Slice) where
|
|||
-/
|
||||
| rejected (startPos endPos : s.Pos)
|
||||
/--
|
||||
The subslice starting at {name}`startPos` and ending at {name}`endPos` did not match the pattern.
|
||||
The subslice starting at {name}`startPos` and ending at {name}`endPos` matches the pattern.
|
||||
-/
|
||||
| matched (startPos endPos : s.Pos)
|
||||
deriving Inhabited
|
||||
|
|
@ -99,44 +99,6 @@ where
|
|||
simp [Pos.Raw.lt_iff] at h ⊢
|
||||
omega
|
||||
|
||||
variable {ρ : Type} {σ : Slice → Type}
|
||||
variable [∀ s, Std.Iterators.Iterator (σ s) Id (SearchStep s)]
|
||||
variable [∀ s, Std.Iterators.Finite (σ s) Id]
|
||||
|
||||
/--
|
||||
Tries to skip the {name}`searcher` until the next {name}`SearchStep.matched` and return it. If no
|
||||
match is found until the end returns {name}`none`.
|
||||
-/
|
||||
@[inline]
|
||||
def nextMatch (searcher : Std.Iter (α := σ s) (SearchStep s)) :
|
||||
Option (Std.Iter (α := σ s) (SearchStep s) × s.Pos × s.Pos) :=
|
||||
go searcher
|
||||
where
|
||||
go [∀ s, Std.Iterators.Finite (σ s) Id] (searcher : Std.Iter (α := σ s) (SearchStep s)) :
|
||||
Option (Std.Iter (α := σ s) (SearchStep s) × s.Pos × s.Pos) :=
|
||||
match searcher.step with
|
||||
| .yield it (.matched startPos endPos) _ => some (it, startPos, endPos)
|
||||
| .yield it (.rejected ..) _ | .skip it .. => go it
|
||||
| .done .. => none
|
||||
termination_by Std.Iterators.Iter.finitelyManySteps searcher
|
||||
|
||||
/--
|
||||
Tries to skip the {name}`searcher` until the next {name}`SearchStep.rejected` and return it. If no
|
||||
reject is found until the end returns {name}`none`.
|
||||
-/
|
||||
@[inline]
|
||||
def nextReject (searcher : Std.Iter (α := σ s) (SearchStep s)) :
|
||||
Option (Std.Iter (α := σ s) (SearchStep s) × s.Pos × s.Pos) :=
|
||||
go searcher
|
||||
where
|
||||
go [∀ s, Std.Iterators.Finite (σ s) Id] (searcher : Std.Iter (α := σ s) (SearchStep s)) :
|
||||
Option (Std.Iter (α := σ s) (SearchStep s) × s.Pos × s.Pos) :=
|
||||
match searcher.step with
|
||||
| .yield it (.rejected startPos endPos) _ => some (it, startPos, endPos)
|
||||
| .yield it (.matched ..) _ | .skip it .. => go it
|
||||
| .done .. => none
|
||||
termination_by Std.Iterators.Iter.finitelyManySteps searcher
|
||||
|
||||
end Internal
|
||||
|
||||
namespace ForwardPattern
|
||||
|
|
|
|||
|
|
@ -112,8 +112,8 @@ Examples:
|
|||
def startsWith [ForwardPattern ρ] (s : Slice) (pat : ρ) : Bool :=
|
||||
ForwardPattern.startsWith s pat
|
||||
|
||||
inductive SplitIterator (ρ : Type) [ToForwardSearcher ρ σ] where
|
||||
| operating (s : Slice) (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
|
||||
inductive SplitIterator (ρ : Type) (s : Slice) [ToForwardSearcher ρ σ] where
|
||||
| operating (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
|
||||
| atEnd
|
||||
deriving Inhabited
|
||||
|
||||
|
|
@ -121,33 +121,72 @@ namespace SplitIterator
|
|||
|
||||
variable [ToForwardSearcher ρ σ]
|
||||
|
||||
instance [Pure m] : Std.Iterators.Iterator (SplitIterator ρ) m Slice where
|
||||
IsPlausibleStep := fun _ _ => True
|
||||
step := fun ⟨iter⟩ =>
|
||||
match iter with
|
||||
| .operating s currPos searcher =>
|
||||
match Internal.nextMatch searcher with
|
||||
| some (searcher, startPos, endPos) =>
|
||||
inductive PlausibleStep
|
||||
|
||||
instance : Std.Iterators.Iterator (SplitIterator ρ s) Id Slice where
|
||||
IsPlausibleStep
|
||||
| ⟨.operating _ s⟩, .yield ⟨.operating _ s'⟩ _ => s'.IsPlausibleSuccessorOf s
|
||||
| ⟨.operating _ s⟩, .yield ⟨.atEnd ..⟩ _ => True
|
||||
| ⟨.operating _ s⟩, .skip ⟨.operating _ s'⟩ => s'.IsPlausibleSuccessorOf s
|
||||
| ⟨.operating _ s⟩, .skip ⟨.atEnd ..⟩ => False
|
||||
| ⟨.operating _ s⟩, .done => True
|
||||
| ⟨.atEnd⟩, .yield .. => False
|
||||
| ⟨.atEnd⟩, .skip _ => False
|
||||
| ⟨.atEnd⟩, .done => True
|
||||
step
|
||||
| ⟨.operating currPos searcher⟩ =>
|
||||
match h : searcher.step with
|
||||
| ⟨.yield searcher' (.matched startPos endPos), hps⟩ =>
|
||||
let slice := s.replaceStartEnd! currPos startPos
|
||||
let nextIt := ⟨.operating s endPos searcher⟩
|
||||
pure (.deflate ⟨.yield nextIt slice, by simp⟩)
|
||||
| none =>
|
||||
let nextIt := ⟨.operating endPos searcher'⟩
|
||||
pure (.deflate ⟨.yield nextIt slice, by simp [nextIt, hps.isPlausibleSuccessor_of_yield]⟩)
|
||||
| ⟨.yield searcher' (.rejected ..), hps⟩ =>
|
||||
pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
|
||||
by simp [hps.isPlausibleSuccessor_of_yield]⟩)
|
||||
| ⟨.skip searcher', hps⟩ =>
|
||||
pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
|
||||
by simp [hps.isPlausibleSuccessor_of_skip]⟩)
|
||||
| ⟨.done, _⟩ =>
|
||||
let slice := s.replaceStart currPos
|
||||
pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
|
||||
| .atEnd => pure (.deflate ⟨.done, by simp⟩)
|
||||
| ⟨.atEnd⟩ => pure (.deflate ⟨.done, by simp⟩)
|
||||
|
||||
-- TODO: Finiteness after we have a notion of lawful searcher
|
||||
private def toOption : SplitIterator ρ s → Option (Std.Iter (α := σ s) (SearchStep s))
|
||||
| .operating _ s => some s
|
||||
| .atEnd => none
|
||||
|
||||
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (SplitIterator ρ) m n :=
|
||||
private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
|
||||
Std.Iterators.FinitenessRelation (SplitIterator ρ s) Id where
|
||||
rel := InvImage (Option.lt Std.Iterators.Iter.IsPlausibleSuccessorOf)
|
||||
(SplitIterator.toOption ∘ Std.Iterators.IterM.internalState)
|
||||
wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
|
||||
subrelation {it it'} h := by
|
||||
simp_wf
|
||||
obtain ⟨step, h, h'⟩ := h
|
||||
match step with
|
||||
| .yield it'' out | .skip it'' =>
|
||||
obtain rfl : it' = it'' := by simpa using h.symm
|
||||
simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
|
||||
revert h'
|
||||
match it, it' with
|
||||
| ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [SplitIterator.toOption, Option.lt]
|
||||
| ⟨.operating _ searcher⟩, ⟨.atEnd⟩ => simp [SplitIterator.toOption, Option.lt]
|
||||
| ⟨.atEnd⟩, _ => simp
|
||||
|
||||
@[no_expose]
|
||||
instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (SplitIterator ρ s) Id :=
|
||||
.of_finitenessRelation finitenessRelation
|
||||
|
||||
instance [Monad n] : Std.Iterators.IteratorCollect (SplitIterator ρ s) Id n :=
|
||||
.defaultImplementation
|
||||
|
||||
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial (SplitIterator ρ) m n :=
|
||||
instance [Monad n] : Std.Iterators.IteratorCollectPartial (SplitIterator ρ s) Id n :=
|
||||
.defaultImplementation
|
||||
|
||||
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (SplitIterator ρ) m n :=
|
||||
instance [Monad n] : Std.Iterators.IteratorLoop (SplitIterator ρ s) Id n :=
|
||||
.defaultImplementation
|
||||
|
||||
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (SplitIterator ρ) m n :=
|
||||
instance [Monad n] : Std.Iterators.IteratorLoopPartial (SplitIterator ρ s) Id n :=
|
||||
.defaultImplementation
|
||||
|
||||
end SplitIterator
|
||||
|
|
@ -161,18 +200,18 @@ multiple subslices in a row match the pattern, the resulting list will contain e
|
|||
This function is generic over all currently supported patterns.
|
||||
|
||||
Examples:
|
||||
* {lean}`("coffee tea water".toSlice.split Char.isWhitespace).allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
|
||||
* {lean}`("coffee tea water".toSlice.split ' ').allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
|
||||
* {lean}`("coffee tea water".toSlice.split " tea ").allowNontermination.toList == ["coffee".toSlice, "water".toSlice]`
|
||||
* {lean}`("ababababa".toSlice.split "aba").allowNontermination.toList == ["coffee".toSlice, "water".toSlice]`
|
||||
* {lean}`("baaab".toSlice.split "aa").allowNontermination.toList == ["b".toSlice, "ab".toSlice]`
|
||||
* {lean}`("coffee tea water".toSlice.split Char.isWhitespace).toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
|
||||
* {lean}`("coffee tea water".toSlice.split ' ').toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
|
||||
* {lean}`("coffee tea water".toSlice.split " tea ").toList == ["coffee".toSlice, "water".toSlice]`
|
||||
* {lean}`("ababababa".toSlice.split "aba").toList == ["coffee".toSlice, "water".toSlice]`
|
||||
* {lean}`("baaab".toSlice.split "aa").toList == ["b".toSlice, "ab".toSlice]`
|
||||
-/
|
||||
@[specialize pat]
|
||||
def split [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Std.Iter (α := SplitIterator ρ) Slice :=
|
||||
{ internalState := .operating s s.startPos (ToForwardSearcher.toSearcher s pat) }
|
||||
def split [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Std.Iter (α := SplitIterator ρ s) Slice :=
|
||||
{ internalState := .operating s.startPos (ToForwardSearcher.toSearcher s pat) }
|
||||
|
||||
inductive SplitInclusiveIterator (ρ : Type) [ToForwardSearcher ρ σ] where
|
||||
| operating (s : Slice) (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
|
||||
inductive SplitInclusiveIterator (ρ : Type) (s : Slice) [ToForwardSearcher ρ σ] where
|
||||
| operating (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
|
||||
| atEnd
|
||||
deriving Inhabited
|
||||
|
||||
|
|
@ -180,40 +219,79 @@ namespace SplitInclusiveIterator
|
|||
|
||||
variable [ToForwardSearcher ρ σ]
|
||||
|
||||
instance [Pure m] : Std.Iterators.Iterator (SplitInclusiveIterator ρ) m Slice where
|
||||
IsPlausibleStep := fun _ _ => True
|
||||
step := fun ⟨iter⟩ =>
|
||||
match iter with
|
||||
| .operating s currPos searcher =>
|
||||
match Internal.nextMatch searcher with
|
||||
| some (searcher, _, endPos) =>
|
||||
instance : Std.Iterators.Iterator (SplitInclusiveIterator ρ s) Id Slice where
|
||||
IsPlausibleStep
|
||||
| ⟨.operating _ s⟩, .yield ⟨.operating _ s'⟩ _ => s'.IsPlausibleSuccessorOf s
|
||||
| ⟨.operating _ s⟩, .yield ⟨.atEnd ..⟩ _ => True
|
||||
| ⟨.operating _ s⟩, .skip ⟨.operating _ s'⟩ => s'.IsPlausibleSuccessorOf s
|
||||
| ⟨.operating _ s⟩, .skip ⟨.atEnd ..⟩ => False
|
||||
| ⟨.operating _ s⟩, .done => True
|
||||
| ⟨.atEnd⟩, .yield .. => False
|
||||
| ⟨.atEnd⟩, .skip _ => False
|
||||
| ⟨.atEnd⟩, .done => True
|
||||
step
|
||||
| ⟨.operating currPos searcher⟩ =>
|
||||
match h : searcher.step with
|
||||
| ⟨.yield searcher' (.matched _ endPos), hps⟩ =>
|
||||
let slice := s.replaceStartEnd! currPos endPos
|
||||
let nextIt := ⟨.operating s endPos searcher⟩
|
||||
pure (.deflate ⟨.yield nextIt slice, by simp⟩)
|
||||
| none =>
|
||||
let nextIt := ⟨.operating endPos searcher'⟩
|
||||
pure (.deflate ⟨.yield nextIt slice,
|
||||
by simp [nextIt, hps.isPlausibleSuccessor_of_yield]⟩)
|
||||
| ⟨.yield searcher' (.rejected ..), hps⟩ =>
|
||||
pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
|
||||
by simp [hps.isPlausibleSuccessor_of_yield]⟩)
|
||||
| ⟨.skip searcher', hps⟩ =>
|
||||
pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
|
||||
by simp [hps.isPlausibleSuccessor_of_skip]⟩)
|
||||
| ⟨.done, _⟩ =>
|
||||
if currPos != s.endPos then
|
||||
let slice := s.replaceStart currPos
|
||||
pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
|
||||
else
|
||||
pure (.deflate ⟨.done, by simp⟩)
|
||||
| .atEnd => pure (.deflate ⟨.done, by simp⟩)
|
||||
| ⟨.atEnd⟩ => pure (.deflate ⟨.done, by simp⟩)
|
||||
|
||||
-- TODO: Finiteness after we have a notion of lawful searcher
|
||||
private def toOption : SplitInclusiveIterator ρ s → Option (Std.Iter (α := σ s) (SearchStep s))
|
||||
| .operating _ s => some s
|
||||
| .atEnd => none
|
||||
|
||||
instance [Monad m] [Monad n] :
|
||||
Std.Iterators.IteratorCollect (SplitInclusiveIterator ρ) m n :=
|
||||
private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
|
||||
Std.Iterators.FinitenessRelation (SplitInclusiveIterator ρ s) Id where
|
||||
rel := InvImage (Option.lt Std.Iterators.Iter.IsPlausibleSuccessorOf)
|
||||
(SplitInclusiveIterator.toOption ∘ Std.Iterators.IterM.internalState)
|
||||
wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
|
||||
subrelation {it it'} h := by
|
||||
simp_wf
|
||||
obtain ⟨step, h, h'⟩ := h
|
||||
match step with
|
||||
| .yield it'' out | .skip it'' =>
|
||||
obtain rfl : it' = it'' := by simpa using h.symm
|
||||
simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
|
||||
revert h'
|
||||
match it, it' with
|
||||
| ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [SplitInclusiveIterator.toOption, Option.lt]
|
||||
| ⟨.operating _ searcher⟩, ⟨.atEnd⟩ => simp [SplitInclusiveIterator.toOption, Option.lt]
|
||||
| ⟨.atEnd⟩, _ => simp
|
||||
|
||||
@[no_expose]
|
||||
instance [Std.Iterators.Finite (σ s) Id] :
|
||||
Std.Iterators.Finite (SplitInclusiveIterator ρ s) Id :=
|
||||
.of_finitenessRelation finitenessRelation
|
||||
|
||||
instance [Monad n] {s} :
|
||||
Std.Iterators.IteratorCollect (SplitInclusiveIterator ρ s) Id n :=
|
||||
.defaultImplementation
|
||||
|
||||
instance [Monad m] [Monad n] :
|
||||
Std.Iterators.IteratorCollectPartial (SplitInclusiveIterator ρ) m n :=
|
||||
instance [Monad n] {s} :
|
||||
Std.Iterators.IteratorCollectPartial (SplitInclusiveIterator ρ s) Id n :=
|
||||
.defaultImplementation
|
||||
|
||||
instance [Monad m] [Monad n] :
|
||||
Std.Iterators.IteratorLoop (SplitInclusiveIterator ρ) m n :=
|
||||
instance [Monad n] {s} :
|
||||
Std.Iterators.IteratorLoop (SplitInclusiveIterator ρ s) Id n :=
|
||||
.defaultImplementation
|
||||
|
||||
instance [Monad m] [Monad n] :
|
||||
Std.Iterators.IteratorLoopPartial (SplitInclusiveIterator ρ) m n :=
|
||||
instance [Monad n] {s} :
|
||||
Std.Iterators.IteratorLoopPartial (SplitInclusiveIterator ρ s) Id n :=
|
||||
.defaultImplementation
|
||||
|
||||
end SplitInclusiveIterator
|
||||
|
|
@ -225,15 +303,15 @@ matched subslices are included at the end of each subslice.
|
|||
This function is generic over all currently supported patterns.
|
||||
|
||||
Examples:
|
||||
* {lean}`("coffee tea water".toSlice.splitInclusive Char.isWhitespace).allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
|
||||
* {lean}`("coffee tea water".toSlice.splitInclusive ' ').allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
|
||||
* {lean}`("coffee tea water".toSlice.splitInclusive " tea ").allowNontermination.toList == ["coffee tea ".toSlice, "water".toSlice]`
|
||||
* {lean}`("baaab".toSlice.splitInclusive "aa").allowNontermination.toList == ["baa".toSlice, "ab".toSlice]`
|
||||
* {lean}`("coffee tea water".toSlice.splitInclusive Char.isWhitespace).toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
|
||||
* {lean}`("coffee tea water".toSlice.splitInclusive ' ').toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
|
||||
* {lean}`("coffee tea water".toSlice.splitInclusive " tea ").toList == ["coffee tea ".toSlice, "water".toSlice]`
|
||||
* {lean}`("baaab".toSlice.splitInclusive "aa").toList == ["baa".toSlice, "ab".toSlice]`
|
||||
-/
|
||||
@[specialize pat]
|
||||
def splitInclusive [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) :
|
||||
Std.Iter (α := SplitInclusiveIterator ρ) Slice :=
|
||||
{ internalState := .operating s s.startPos (ToForwardSearcher.toSearcher s pat) }
|
||||
Std.Iter (α := SplitInclusiveIterator ρ s) Slice :=
|
||||
{ internalState := .operating s.startPos (ToForwardSearcher.toSearcher s pat) }
|
||||
|
||||
/--
|
||||
If {name}`pat` matches a prefix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
|
||||
|
|
@ -384,9 +462,7 @@ Examples:
|
|||
@[specialize pat]
|
||||
def find? [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Option s.Pos :=
|
||||
let searcher := ToForwardSearcher.toSearcher s pat
|
||||
match Internal.nextMatch searcher with
|
||||
| some (_, startPos, _) => some startPos
|
||||
| none => none
|
||||
searcher.findSome? (fun | .matched startPos _ => some startPos | .rejected .. => none)
|
||||
|
||||
/--
|
||||
Checks whether a slice has a match of the pattern {name}`pat` anywhere.
|
||||
|
|
@ -401,7 +477,7 @@ Examples:
|
|||
@[specialize pat]
|
||||
def contains [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Bool :=
|
||||
let searcher := ToForwardSearcher.toSearcher s pat
|
||||
Internal.nextMatch searcher |>.isSome
|
||||
searcher.any (· matches .matched ..)
|
||||
|
||||
/--
|
||||
Checks whether a slice only consists of matches of the pattern {name}`pat` anywhere.
|
||||
|
|
@ -415,6 +491,7 @@ Examples:
|
|||
* {lean}`"brown and orange".toSlice.all Char.isLower = false`
|
||||
* {lean}`"aaaaaa".toSlice.all 'a' = true`
|
||||
* {lean}`"aaaaaa".toSlice.all "aa" = true`
|
||||
* {lean}`"aaaaaaa".toSlice.all "aa" = false`
|
||||
-/
|
||||
@[inline]
|
||||
def all [ForwardPattern ρ] (s : Slice) (pat : ρ) : Bool :=
|
||||
|
|
@ -445,8 +522,8 @@ Examples:
|
|||
def endsWith [BackwardPattern ρ] (s : Slice) (pat : ρ) : Bool :=
|
||||
BackwardPattern.endsWith s pat
|
||||
|
||||
inductive RevSplitIterator (ρ : Type) [ToBackwardSearcher ρ σ] where
|
||||
| operating (s : Slice) (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
|
||||
inductive RevSplitIterator (ρ : Type) (s : Slice) [ToBackwardSearcher ρ σ] where
|
||||
| operating (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
|
||||
| atEnd
|
||||
deriving Inhabited
|
||||
|
||||
|
|
@ -454,37 +531,74 @@ namespace RevSplitIterator
|
|||
|
||||
variable [ToBackwardSearcher ρ σ]
|
||||
|
||||
instance [Pure m] : Std.Iterators.Iterator (RevSplitIterator ρ) m Slice where
|
||||
IsPlausibleStep := fun _ _ => True
|
||||
step := fun ⟨iter⟩ =>
|
||||
match iter with
|
||||
| .operating s currPos searcher =>
|
||||
match Internal.nextMatch searcher with
|
||||
| some (searcher, startPos, endPos) =>
|
||||
instance [Pure m] : Std.Iterators.Iterator (RevSplitIterator ρ s) m Slice where
|
||||
IsPlausibleStep
|
||||
| ⟨.operating _ s⟩, .yield ⟨.operating _ s'⟩ _ => s'.IsPlausibleSuccessorOf s
|
||||
| ⟨.operating _ s⟩, .yield ⟨.atEnd ..⟩ _ => True
|
||||
| ⟨.operating _ s⟩, .skip ⟨.operating _ s'⟩ => s'.IsPlausibleSuccessorOf s
|
||||
| ⟨.operating _ s⟩, .skip ⟨.atEnd ..⟩ => False
|
||||
| ⟨.operating _ s⟩, .done => True
|
||||
| ⟨.atEnd⟩, .yield .. => False
|
||||
| ⟨.atEnd⟩, .skip _ => False
|
||||
| ⟨.atEnd⟩, .done => True
|
||||
step
|
||||
| ⟨.operating currPos searcher⟩ =>
|
||||
match h : searcher.step with
|
||||
| ⟨.yield searcher' (.matched startPos endPos), hps⟩ =>
|
||||
let slice := s.replaceStartEnd! endPos currPos
|
||||
let nextIt := ⟨.operating s startPos searcher⟩
|
||||
pure (.deflate ⟨.yield nextIt slice, by simp⟩)
|
||||
| none =>
|
||||
let nextIt := ⟨.operating startPos searcher'⟩
|
||||
pure (.deflate ⟨.yield nextIt slice, by simp [nextIt, hps.isPlausibleSuccessor_of_yield]⟩)
|
||||
| ⟨.yield searcher' (.rejected ..), hps⟩ =>
|
||||
pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
|
||||
by simp [hps.isPlausibleSuccessor_of_yield]⟩)
|
||||
| ⟨.skip searcher', hps⟩ =>
|
||||
pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
|
||||
by simp [hps.isPlausibleSuccessor_of_skip]⟩)
|
||||
| ⟨.done, _⟩ =>
|
||||
if currPos ≠ s.startPos then
|
||||
let slice := s.replaceEnd currPos
|
||||
pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
|
||||
else
|
||||
pure (.deflate ⟨.done, by simp⟩)
|
||||
| .atEnd => pure (.deflate ⟨.done, by simp⟩)
|
||||
| ⟨.atEnd⟩ => pure (.deflate ⟨.done, by simp⟩)
|
||||
|
||||
-- TODO: Finiteness after we have a notion of lawful searcher
|
||||
private def toOption : RevSplitIterator ρ s → Option (Std.Iter (α := σ s) (SearchStep s))
|
||||
| .operating _ s => some s
|
||||
| .atEnd => none
|
||||
|
||||
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevSplitIterator ρ) m n :=
|
||||
private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
|
||||
Std.Iterators.FinitenessRelation (RevSplitIterator ρ s) Id where
|
||||
rel := InvImage (Option.lt Std.Iterators.Iter.IsPlausibleSuccessorOf)
|
||||
(RevSplitIterator.toOption ∘ Std.Iterators.IterM.internalState)
|
||||
wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
|
||||
subrelation {it it'} h := by
|
||||
simp_wf
|
||||
obtain ⟨step, h, h'⟩ := h
|
||||
match step with
|
||||
| .yield it'' out | .skip it'' =>
|
||||
obtain rfl : it' = it'' := by simpa using h.symm
|
||||
simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
|
||||
revert h'
|
||||
match it, it' with
|
||||
| ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [RevSplitIterator.toOption, Option.lt]
|
||||
| ⟨.operating _ searcher⟩, ⟨.atEnd⟩ => simp [RevSplitIterator.toOption, Option.lt]
|
||||
| ⟨.atEnd⟩, _ => simp
|
||||
|
||||
@[no_expose]
|
||||
instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (RevSplitIterator ρ s) Id :=
|
||||
.of_finitenessRelation finitenessRelation
|
||||
|
||||
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevSplitIterator ρ s) m n :=
|
||||
.defaultImplementation
|
||||
|
||||
instance [Monad m] [Monad n] :
|
||||
Std.Iterators.IteratorCollectPartial (RevSplitIterator ρ) m n :=
|
||||
Std.Iterators.IteratorCollectPartial (RevSplitIterator ρ s) m n :=
|
||||
.defaultImplementation
|
||||
|
||||
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevSplitIterator ρ) m n :=
|
||||
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevSplitIterator ρ s) m n :=
|
||||
.defaultImplementation
|
||||
|
||||
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RevSplitIterator ρ) m n :=
|
||||
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RevSplitIterator ρ s) m n :=
|
||||
.defaultImplementation
|
||||
|
||||
end RevSplitIterator
|
||||
|
|
@ -500,13 +614,13 @@ This function is generic over all currently supported patterns except
|
|||
{name}`String`/{name}`String.Slice`.
|
||||
|
||||
Examples:
|
||||
* {lean}`("coffee tea water".toSlice.revSplit Char.isWhitespace).allowNontermination.toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`
|
||||
* {lean}`("coffee tea water".toSlice.revSplit ' ').allowNontermination.toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`
|
||||
* {lean}`("coffee tea water".toSlice.revSplit Char.isWhitespace).toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`
|
||||
* {lean}`("coffee tea water".toSlice.revSplit ' ').toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`
|
||||
-/
|
||||
@[specialize pat]
|
||||
def revSplit [ToBackwardSearcher ρ σ] (s : Slice) (pat : ρ) :
|
||||
Std.Iter (α := RevSplitIterator ρ) Slice :=
|
||||
{ internalState := .operating s s.endPos (ToBackwardSearcher.toSearcher s pat) }
|
||||
Std.Iter (α := RevSplitIterator ρ s) Slice :=
|
||||
{ internalState := .operating s.endPos (ToBackwardSearcher.toSearcher s pat) }
|
||||
|
||||
/--
|
||||
If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
|
||||
|
|
@ -658,9 +772,7 @@ Examples:
|
|||
@[specialize pat]
|
||||
def revFind? [ToBackwardSearcher ρ σ] (s : Slice) (pat : ρ) : Option s.Pos :=
|
||||
let searcher := ToBackwardSearcher.toSearcher s pat
|
||||
match Internal.nextMatch searcher with
|
||||
| some (_, startPos, _) => some startPos
|
||||
| none => none
|
||||
searcher.findSome? (fun | .matched startPos _ => some startPos | .rejected .. => none)
|
||||
|
||||
end BackwardPatternUsers
|
||||
|
||||
|
|
@ -1048,9 +1160,9 @@ Creates an iterator over all lines in {name}`s` with the line ending characters
|
|||
stripped.
|
||||
|
||||
Examples:
|
||||
* {lean}`"foo\r\nbar\n\nbaz\n".toSlice.lines.allowNontermination.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`
|
||||
* {lean}`"foo\r\nbar\n\nbaz".toSlice.lines.allowNontermination.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`
|
||||
* {lean}`"foo\r\nbar\n\nbaz\r".toSlice.lines.allowNontermination.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]`
|
||||
* {lean}`"foo\r\nbar\n\nbaz\n".toSlice.lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`
|
||||
* {lean}`"foo\r\nbar\n\nbaz".toSlice.lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`
|
||||
* {lean}`"foo\r\nbar\n\nbaz\r".toSlice.lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]`
|
||||
-/
|
||||
def lines (s : Slice) :=
|
||||
s.splitInclusive '\n' |>.map lines.lineMap
|
||||
|
|
|
|||
|
|
@ -19,16 +19,16 @@ Tests for `String.Slice` functions
|
|||
#guard "red green blue".toSlice.startsWith 'r' = true
|
||||
#guard "red green blue".toSlice.startsWith Char.isLower = true
|
||||
|
||||
#guard ("coffee tea water".toSlice.split Char.isWhitespace).allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]
|
||||
#guard ("coffee tea water".toSlice.split ' ').allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]
|
||||
#guard ("coffee tea water".toSlice.split " tea ").allowNontermination.toList == ["coffee".toSlice, "water".toSlice]
|
||||
#guard ("baaab".toSlice.split "aa").allowNontermination.toList == ["b".toSlice, "ab".toSlice]
|
||||
#guard ("coffee tea water".toSlice.split Char.isWhitespace).toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]
|
||||
#guard ("coffee tea water".toSlice.split ' ').toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]
|
||||
#guard ("coffee tea water".toSlice.split " tea ").toList == ["coffee".toSlice, "water".toSlice]
|
||||
#guard ("baaab".toSlice.split "aa").toList == ["b".toSlice, "ab".toSlice]
|
||||
|
||||
#guard ("coffee tea water".toSlice.splitInclusive Char.isWhitespace).allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
|
||||
#guard ("coffee tea water".toSlice.splitInclusive ' ').allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
|
||||
#guard ("coffee tea water".toSlice.splitInclusive " tea ").allowNontermination.toList == ["coffee tea ".toSlice, "water".toSlice]
|
||||
#guard ("a".toSlice.splitInclusive (fun (_ : Char) => true)).allowNontermination.toList == ["a".toSlice]
|
||||
#guard ("baaab".toSlice.splitInclusive "aa").allowNontermination.toList == ["baa".toSlice, "ab".toSlice]
|
||||
#guard ("coffee tea water".toSlice.splitInclusive Char.isWhitespace).toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
|
||||
#guard ("coffee tea water".toSlice.splitInclusive ' ').toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
|
||||
#guard ("coffee tea water".toSlice.splitInclusive " tea ").toList == ["coffee tea ".toSlice, "water".toSlice]
|
||||
#guard ("a".toSlice.splitInclusive (fun (_ : Char) => true)).toList == ["a".toSlice]
|
||||
#guard ("baaab".toSlice.splitInclusive "aa").toList == ["baa".toSlice, "ab".toSlice]
|
||||
|
||||
#guard "red green blue".toSlice.drop 4 == "green blue".toSlice
|
||||
#guard "red green blue".toSlice.drop 10 == "blue".toSlice
|
||||
|
|
@ -77,6 +77,7 @@ Tests for `String.Slice` functions
|
|||
#guard "brown and orange".toSlice.all Char.isLower = false
|
||||
#guard "aaaaaa".toSlice.all 'a' = true
|
||||
#guard "aaaaaa".toSlice.all "aa" = true
|
||||
#guard "aaaaaaa".toSlice.all "aa" = false
|
||||
|
||||
#guard "red green blue".toSlice.endsWith "blue" = true
|
||||
#guard "red green blue".toSlice.endsWith "green" = false
|
||||
|
|
@ -84,8 +85,8 @@ Tests for `String.Slice` functions
|
|||
#guard "red green blue".toSlice.endsWith 'e' = true
|
||||
#guard "red green blue".toSlice.endsWith Char.isLower = true
|
||||
|
||||
#guard ("coffee tea water".toSlice.revSplit Char.isWhitespace).allowNontermination.toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]
|
||||
#guard ("coffee tea water".toSlice.revSplit ' ').allowNontermination.toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]
|
||||
#guard ("coffee tea water".toSlice.revSplit Char.isWhitespace).toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]
|
||||
#guard ("coffee tea water".toSlice.revSplit ' ').toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]
|
||||
|
||||
#guard "red green blue".toSlice.dropEnd 5 == "red green".toSlice
|
||||
#guard "red green blue".toSlice.dropEnd 11 == "red".toSlice
|
||||
|
|
@ -158,9 +159,9 @@ Tests for `String.Slice` functions
|
|||
#guard "abc".toSlice.revBytes.toList = [99, 98, 97]
|
||||
#guard "ab∀c".toSlice.revBytes.toList = [99, 128, 136, 226, 98, 97]
|
||||
|
||||
#guard "foo\r\nbar\n\nbaz\n".toSlice.lines.allowNontermination.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]
|
||||
#guard "foo\r\nbar\n\nbaz".toSlice.lines.allowNontermination.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]
|
||||
#guard "foo\r\nbar\n\nbaz\r".toSlice.lines.allowNontermination.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]
|
||||
#guard "foo\r\nbar\n\nbaz\n".toSlice.lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]
|
||||
#guard "foo\r\nbar\n\nbaz".toSlice.lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]
|
||||
#guard "foo\r\nbar\n\nbaz\r".toSlice.lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]
|
||||
|
||||
#guard "coffee tea water".toSlice.foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 2
|
||||
#guard "coffee tea and water".toSlice.foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue