Skip to content

Commit 8cc180a

Browse files
TwoFXTwoFX
committed
more
1 parent c0efa39 commit 8cc180a

File tree

2 files changed

+84
-39
lines changed

2 files changed

+84
-39
lines changed

‎src/Init/Data/String/Slice.lean‎

Lines changed: 74 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -112,42 +112,86 @@ Examples:
112112
def startsWith [ForwardPattern ρ] (s : Slice) (pat : ρ) : Bool :=
113113
ForwardPattern.startsWith s pat
114114

115-
inductive SplitIterator (ρ : Type) [ToForwardSearcher ρ σ] where
116-
| operating (s : Slice) (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
115+
inductive SplitIterator (ρ : Type) (s : Slice) [ToForwardSearcher ρ σ] where
116+
| operating (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
117117
| atEnd
118118
deriving Inhabited
119119

120120
namespace SplitIterator
121121

122122
variable [ToForwardSearcher ρ σ]
123123

124-
instance [Pure m] : Std.Iterators.Iterator (SplitIterator ρ) m Slice where
125-
IsPlausibleStep := fun _ _ => True
124+
instance [Pure m] : Std.Iterators.Iterator (SplitIterator ρ s) m Slice where
125+
IsPlausibleStep it
126+
| .yield it' out =>
127+
match it.internalState, it'.internalState with
128+
| .operating _ searcher, .operating _ searcher' =>
129+
searcher'.finitelyManySteps.Rel searcher.finitelyManySteps
130+
| .operating _ searcher, .atEnd => True
131+
| .atEnd, _ => False
132+
| .skip _ => False
133+
| .done => True
126134
step := fun ⟨iter⟩ =>
127135
match iter with
128-
| .operating s currPos searcher =>
129-
match Internal.nextMatch searcher with
136+
| .operating currPos searcher =>
137+
match h : Internal.nextMatch searcher with
130138
| some (searcher, startPos, endPos) =>
131139
let slice := s.replaceStartEnd! currPos startPos
132-
let nextIt := ⟨.operating s endPos searcher⟩
133-
pure (.deflate ⟨.yield nextIt slice, by simp⟩)
140+
let nextIt := ⟨.operating endPos searcher⟩
141+
pure (.deflate ⟨.yield nextIt slice,
142+
by simpa [nextIt] using Pattern.Internal.finitelyManySteps_rel_nextMatch h⟩)
134143
| none =>
135144
let slice := s.replaceStart currPos
136145
pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
137146
| .atEnd => pure (.deflate ⟨.done, by simp⟩)
138147

139-
-- TODO: Finiteness after we have a notion of lawful searcher
148+
private def toOption : SplitIterator ρ s → Option (Std.Iter (α := σ s) (SearchStep s))
149+
| .operating _ s => some s
150+
| .atEnd => none
140151

141-
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (SplitIterator ρ) m n :=
152+
private instance {s} [Std.Iterators.Finite (σ s) Id] :
153+
WellFoundedRelation (SplitIterator ρ s) where
154+
rel := InvImage (Option.lt (InvImage Std.Iterators.IterM.TerminationMeasures.Finite.Rel
155+
Std.Iterators.Iter.finitelyManySteps)) SplitIterator.toOption
156+
wf := by
157+
apply InvImage.wf
158+
apply Option.wellFounded_lt
159+
apply InvImage.wf
160+
exact WellFoundedRelation.wf
161+
162+
private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
163+
Std.Iterators.FinitenessRelation (SplitIterator ρ s) Id where
164+
rel := InvImage WellFoundedRelation.rel (fun it => it.internalState)
165+
wf := InvImage.wf _ WellFoundedRelation.wf
166+
subrelation {it it'} h := by
167+
simp_wf
168+
obtain ⟨step, h, h'⟩ := h
169+
match step with
170+
| .yield it'' out =>
171+
obtain rfl : it' = it'' := by simpa [Std.Iterators.IterStep.successor] using h.symm
172+
simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
173+
revert h'
174+
match it.internalState, it'.internalState with
175+
| .operating _ searcher, .operating _ searcher' =>
176+
simp [SplitIterator.toOption, Option.lt]
177+
| .operating _ searcher, .atEnd =>
178+
simp [SplitIterator.toOption, Option.lt]
179+
| .atEnd, _ => simp
180+
181+
@[no_expose]
182+
instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (SplitIterator ρ s) Id :=
183+
.of_finitenessRelation finitenessRelation
184+
185+
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (SplitIterator ρ s) m n :=
142186
.defaultImplementation
143187

144-
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial (SplitIterator ρ) m n :=
188+
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial (SplitIterator ρ s) m n :=
145189
.defaultImplementation
146190

147-
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (SplitIterator ρ) m n :=
191+
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (SplitIterator ρ s) m n :=
148192
.defaultImplementation
149193

150-
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (SplitIterator ρ) m n :=
194+
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (SplitIterator ρ s) m n :=
151195
.defaultImplementation
152196

153197
end SplitIterator
@@ -161,15 +205,15 @@ multiple subslices in a row match the pattern, the resulting list will contain e
161205
This function is generic over all currently supported patterns.
162206
163207
Examples:
164-
* {lean}`("coffee tea water".toSlice.split Char.isWhitespace).allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
165-
* {lean}`("coffee tea water".toSlice.split ' ').allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
166-
* {lean}`("coffee tea water".toSlice.split " tea ").allowNontermination.toList == ["coffee".toSlice, "water".toSlice]`
167-
* {lean}`("ababababa".toSlice.split "aba").allowNontermination.toList == ["coffee".toSlice, "water".toSlice]`
168-
* {lean}`("baaab".toSlice.split "aa").allowNontermination.toList == ["b".toSlice, "ab".toSlice]`
208+
* {lean}`("coffee tea water".toSlice.split Char.isWhitespace).toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
209+
* {lean}`("coffee tea water".toSlice.split ' ').toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
210+
* {lean}`("coffee tea water".toSlice.split " tea ").toList == ["coffee".toSlice, "water".toSlice]`
211+
* {lean}`("ababababa".toSlice.split "aba").toList == ["coffee".toSlice, "water".toSlice]`
212+
* {lean}`("baaab".toSlice.split "aa").toList == ["b".toSlice, "ab".toSlice]`
169213
-/
170214
@[specialize pat]
171-
def split [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Std.Iter (α := SplitIterator ρ) Slice :=
172-
{ internalState := .operating s s.startPos (ToForwardSearcher.toSearcher s pat) }
215+
def split [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Std.Iter (α := SplitIterator ρ s) Slice :=
216+
{ internalState := .operating s.startPos (ToForwardSearcher.toSearcher s pat) }
173217

174218
inductive SplitInclusiveIterator (ρ : Type) (s : Slice) [ToForwardSearcher ρ σ] where
175219
| operating (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
@@ -211,8 +255,10 @@ private def toOption : SplitInclusiveIterator ρ s → Option (Std.Iter (α :=
211255
| .operating _ s => some s
212256
| .atEnd => none
213257

214-
private instance {s} [Std.Iterators.Finite (σ s) Id] : WellFoundedRelation (SplitInclusiveIterator ρ s) where
215-
rel := InvImage (Option.lt (InvImage Std.Iterators.IterM.TerminationMeasures.Finite.Rel Std.Iterators.Iter.finitelyManySteps)) SplitInclusiveIterator.toOption
258+
private instance {s} [Std.Iterators.Finite (σ s) Id] :
259+
WellFoundedRelation (SplitInclusiveIterator ρ s) where
260+
rel := InvImage (Option.lt (InvImage Std.Iterators.IterM.TerminationMeasures.Finite.Rel
261+
Std.Iterators.Iter.finitelyManySteps)) SplitInclusiveIterator.toOption
216262
wf := by
217263
apply InvImage.wf
218264
apply Option.wellFounded_lt
@@ -239,11 +285,10 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
239285
| .atEnd, _ => simp
240286

241287
@[no_expose]
242-
instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (SplitInclusiveIterator ρ s) Id :=
288+
instance [Std.Iterators.Finite (σ s) Id] :
289+
Std.Iterators.Finite (SplitInclusiveIterator ρ s) Id :=
243290
.of_finitenessRelation finitenessRelation
244291

245-
-- TODO: Finiteness after we have a notion of lawful searcher
246-
247292
instance [Monad m] [Monad n] {s} :
248293
Std.Iterators.IteratorCollect (SplitInclusiveIterator ρ s) m n :=
249294
.defaultImplementation
@@ -269,10 +314,10 @@ matched subslices are included at the end of each subslice.
269314
This function is generic over all currently supported patterns.
270315
271316
Examples:
272-
* {lean}`("coffee tea water".toSlice.splitInclusive Char.isWhitespace).allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
273-
* {lean}`("coffee tea water".toSlice.splitInclusive ' ').allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
274-
* {lean}`("coffee tea water".toSlice.splitInclusive " tea ").allowNontermination.toList == ["coffee tea ".toSlice, "water".toSlice]`
275-
* {lean}`("baaab".toSlice.splitInclusive "aa").allowNontermination.toList == ["baa".toSlice, "ab".toSlice]`
317+
* {lean}`("coffee tea water".toSlice.splitInclusive Char.isWhitespace).toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
318+
* {lean}`("coffee tea water".toSlice.splitInclusive ' ').toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
319+
* {lean}`("coffee tea water".toSlice.splitInclusive " tea ").toList == ["coffee tea ".toSlice, "water".toSlice]`
320+
* {lean}`("baaab".toSlice.splitInclusive "aa").toList == ["baa".toSlice, "ab".toSlice]`
276321
-/
277322
@[specialize pat]
278323
def splitInclusive [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) :

‎tests/lean/run/string_slice.lean‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -19,16 +19,16 @@ Tests for `String.Slice` functions
1919
#guard "red green blue".toSlice.startsWith 'r' = true
2020
#guard "red green blue".toSlice.startsWith Char.isLower = true
2121

22-
#guard ("coffee tea water".toSlice.split Char.isWhitespace).allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]
23-
#guard ("coffee tea water".toSlice.split ' ').allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]
24-
#guard ("coffee tea water".toSlice.split " tea ").allowNontermination.toList == ["coffee".toSlice, "water".toSlice]
25-
#guard ("baaab".toSlice.split "aa").allowNontermination.toList == ["b".toSlice, "ab".toSlice]
26-
27-
#guard ("coffee tea water".toSlice.splitInclusive Char.isWhitespace).allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
28-
#guard ("coffee tea water".toSlice.splitInclusive ' ').allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
29-
#guard ("coffee tea water".toSlice.splitInclusive " tea ").allowNontermination.toList == ["coffee tea ".toSlice, "water".toSlice]
30-
#guard ("a".toSlice.splitInclusive (fun (_ : Char) => true)).allowNontermination.toList == ["a".toSlice]
31-
#guard ("baaab".toSlice.splitInclusive "aa").allowNontermination.toList == ["baa".toSlice, "ab".toSlice]
22+
#guard ("coffee tea water".toSlice.split Char.isWhitespace).toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]
23+
#guard ("coffee tea water".toSlice.split ' ').toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]
24+
#guard ("coffee tea water".toSlice.split " tea ").toList == ["coffee".toSlice, "water".toSlice]
25+
#guard ("baaab".toSlice.split "aa").toList == ["b".toSlice, "ab".toSlice]
26+
27+
#guard ("coffee tea water".toSlice.splitInclusive Char.isWhitespace).toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
28+
#guard ("coffee tea water".toSlice.splitInclusive ' ').toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
29+
#guard ("coffee tea water".toSlice.splitInclusive " tea ").toList == ["coffee tea ".toSlice, "water".toSlice]
30+
#guard ("a".toSlice.splitInclusive (fun (_ : Char) => true)).toList == ["a".toSlice]
31+
#guard ("baaab".toSlice.splitInclusive "aa").toList == ["baa".toSlice, "ab".toSlice]
3232

3333
#guard "red green blue".toSlice.drop 4 == "green blue".toSlice
3434
#guard "red green blue".toSlice.drop 10 == "blue".toSlice

0 commit comments

Comments
 (0)