feat: move String positions between slices (#11380)
This PR renames `String.Slice.Pos.ofSlice` to `String.Pos.ofToSlice` to adhere with the (yet-to-be documented) naming convention for mapping positions to positions. It then adds several new functions so that for every way to construct a slice from a string and slice, there are now functions for mapping positions forwards and backwards along this construction.
This commit is contained in:
Markus Himmel
GitHub
parent
9ce8a062ba
commit
d8913f88dc
2 changed files with 171 additions and 55 deletions
|
|
@ -1104,7 +1104,7 @@ def Slice.slice? (s : Slice) (newStart newEnd : s.Pos) : Option Slice :=
|
|||
/-- Given a slice and two valid positions within the slice, obtain a new slice on the same underlying
|
||||
string formed by the new bounds, or panic if the given end is strictly less than the given start. -/
|
||||
def Slice.slice! (s : Slice) (newStart newEnd : s.Pos) : Slice :=
|
||||
if h : newStart.offset ≤ newEnd.offset then
|
||||
if h : newStart ≤ newEnd then
|
||||
s.slice newStart newEnd h
|
||||
else
|
||||
panic! "Starting position must be less than or equal to end position."
|
||||
|
|
@ -1219,12 +1219,12 @@ theorem Pos.offset_toSlice {s : String} {pos : s.Pos} : pos.toSlice.offset = pos
|
|||
/-- Given a string `s`, turns a valid position on the slice `s.toSlice` into a valid position on the
|
||||
string `s`. -/
|
||||
@[inline, expose]
|
||||
def Slice.Pos.ofSlice {s : String} (pos : s.toSlice.Pos) : s.Pos where
|
||||
def Pos.ofToSlice {s : String} (pos : s.toSlice.Pos) : s.Pos where
|
||||
offset := pos.offset
|
||||
isValid := pos.isValidForSlice.ofSlice
|
||||
|
||||
@[simp]
|
||||
theorem Slice.Pos.offset_ofSlice {s : String} {pos : s.toSlice.Pos} : pos.ofSlice.offset = pos.offset := (rfl)
|
||||
theorem Pos.offset_ofToSlice {s : String} {pos : s.toSlice.Pos} : (ofToSlice pos).offset = pos.offset := (rfl)
|
||||
|
||||
@[simp]
|
||||
theorem rawEndPos_toSlice {s : String} : s.toSlice.rawEndPos = s.rawEndPos := by
|
||||
|
|
@ -1239,25 +1239,25 @@ theorem startPos_toSlice {s : String} : s.toSlice.startPos = s.startPos.toSlice
|
|||
Slice.Pos.ext (by simp)
|
||||
|
||||
@[simp]
|
||||
theorem Pos.ofSlice_toSlice {s : String} (pos : s.Pos) : pos.toSlice.ofSlice = pos :=
|
||||
theorem Pos.ofToSlice_toSlice {s : String} (pos : s.Pos) : (ofToSlice pos.toSlice) = pos :=
|
||||
Pos.ext (by simp)
|
||||
|
||||
@[simp]
|
||||
theorem Slice.Pos.toSlice_ofSlice {s : String} (pos : s.toSlice.Pos) : pos.ofSlice.toSlice = pos :=
|
||||
theorem Slice.Pos.toSlice_ofToSlice {s : String} (pos : s.toSlice.Pos) : (Pos.ofToSlice pos).toSlice = pos :=
|
||||
Slice.Pos.ext (by simp)
|
||||
|
||||
@[simp]
|
||||
theorem Slice.Pos.toSlice_comp_ofSlice {s : String} :
|
||||
Pos.toSlice ∘ (ofSlice (s := s)) = id := by ext; simp
|
||||
theorem Pos.toSlice_comp_ofToSlice {s : String} :
|
||||
Pos.toSlice ∘ (Pos.ofToSlice (s := s)) = id := by ext; simp
|
||||
|
||||
@[simp]
|
||||
theorem Pos.ofSlice_comp_toSlice {s : String} :
|
||||
Slice.Pos.ofSlice ∘ (toSlice (s := s)) = id := by ext; simp
|
||||
theorem Pos.ofToSlice_comp_toSlice {s : String} :
|
||||
Pos.ofToSlice ∘ (toSlice (s := s)) = id := by ext; simp
|
||||
|
||||
theorem Pos.toSlice_inj {s : String} {p q : s.Pos} : p.toSlice = q.toSlice ↔ p = q :=
|
||||
⟨fun h => by simpa using congrArg Slice.Pos.ofSlice h, (· ▸ rfl)⟩
|
||||
⟨fun h => by simpa using congrArg Pos.ofToSlice h, (· ▸ rfl)⟩
|
||||
|
||||
theorem Slice.Pos.ofSlice_inj {s : String} {p q : s.toSlice.Pos} : p.ofSlice = q.ofSlice ↔ p = q :=
|
||||
theorem Pos.ofToSlice_inj {s : String} {p q : s.toSlice.Pos} : ofToSlice p = ofToSlice q ↔ p = q :=
|
||||
⟨fun h => by simpa using congrArg Pos.toSlice h, (· ▸ rfl)⟩
|
||||
|
||||
@[simp]
|
||||
|
|
@ -1265,18 +1265,18 @@ theorem Pos.toSlice_le {s : String} {p q : s.Pos} : p.toSlice ≤ q.toSlice ↔
|
|||
simp [le_iff, Slice.Pos.le_iff]
|
||||
|
||||
@[simp]
|
||||
theorem Slice.Pos.ofSlice_le {s : String} {p q : s.toSlice.Pos} :
|
||||
p.ofSlice ≤ q.ofSlice ↔ p ≤ q := by
|
||||
simp [String.Pos.le_iff, le_iff]
|
||||
theorem Pos.ofToSlice_le {s : String} {p q : s.toSlice.Pos} :
|
||||
ofToSlice p ≤ ofToSlice q ↔ p ≤ q := by
|
||||
simp [le_iff, Slice.Pos.le_iff]
|
||||
|
||||
@[simp]
|
||||
theorem Pos.toSlice_lt {s : String} {p q : s.Pos} : p.toSlice < q.toSlice ↔ p < q := by
|
||||
simp [lt_iff, Slice.Pos.lt_iff]
|
||||
|
||||
@[simp]
|
||||
theorem Slice.Pos.ofSlice_lt {s : String} {p q : s.toSlice.Pos} :
|
||||
p.ofSlice < q.ofSlice ↔ p < q := by
|
||||
simp [String.Pos.lt_iff, lt_iff]
|
||||
theorem Pos.ofToSlice_lt {s : String} {p q : s.toSlice.Pos} :
|
||||
ofToSlice p < ofToSlice q ↔ p < q := by
|
||||
simp [lt_iff, Slice.Pos.lt_iff]
|
||||
|
||||
/--
|
||||
Returns the character at the position `pos` of a string, taking a proof that `p` is not the
|
||||
|
|
@ -1290,7 +1290,7 @@ Examples:
|
|||
-/
|
||||
@[inline, expose]
|
||||
def Pos.get {s : String} (pos : s.Pos) (h : pos ≠ s.endPos) : Char :=
|
||||
pos.toSlice.get (ne_of_apply_ne Slice.Pos.ofSlice (by simp [h]))
|
||||
pos.toSlice.get (ne_of_apply_ne Pos.ofToSlice (by simp [h]))
|
||||
|
||||
/--
|
||||
Returns the character at the position `pos` of a string, or `none` if the position is the
|
||||
|
|
@ -1317,7 +1317,7 @@ Returns the byte at the position `pos` of a string.
|
|||
-/
|
||||
@[inline, expose]
|
||||
def Pos.byte {s : String} (pos : s.Pos) (h : pos ≠ s.endPos) : UInt8 :=
|
||||
pos.toSlice.byte (ne_of_apply_ne Slice.Pos.ofSlice (by simp [h]))
|
||||
pos.toSlice.byte (ne_of_apply_ne Pos.ofToSlice (by simp [h]))
|
||||
|
||||
theorem Pos.isUTF8FirstByte_byte {s : String} {pos : s.Pos} {h : pos ≠ s.endPos} :
|
||||
(pos.byte h).IsUTF8FirstByte :=
|
||||
|
|
@ -1661,60 +1661,56 @@ def Slice.pos! (s : Slice) (off : String.Pos.Raw) : s.Pos :=
|
|||
position is not the past-the-end position, which guarantees that such a position exists. -/
|
||||
@[expose, extern "lean_string_utf8_next_fast"]
|
||||
def Pos.next {s : @& String} (pos : @& s.Pos) (h : pos ≠ s.endPos) : s.Pos :=
|
||||
(Slice.Pos.next pos.toSlice (ne_of_apply_ne Slice.Pos.ofSlice (by simpa))).ofSlice
|
||||
ofToSlice (Slice.Pos.next pos.toSlice (ne_of_apply_ne Pos.ofToSlice (by simpa)))
|
||||
|
||||
@[simp]
|
||||
theorem Slice.Pos.str_inj {s : Slice} (p₁ p₂ : s.Pos) : p₁.str = p₂.str ↔ p₁ = p₂ := by
|
||||
simp [Slice.Pos.ext_iff, String.Pos.ext_iff, Pos.Raw.ext_iff]
|
||||
|
||||
@[expose, extern "lean_string_utf8_next_fast"]
|
||||
def String.Pos.next {s : @& String} (pos : @& s.Pos) (h : pos ≠ s.endPos) : s.Pos :=
|
||||
(Slice.Pos.next pos.toSlice (ne_of_apply_ne Slice.Pos.ofSlice (by simpa))).ofSlice
|
||||
|
||||
/-- Advances a valid position on a string to the next valid position, or returns `none` if the
|
||||
given position is the past-the-end position. -/
|
||||
@[inline, expose]
|
||||
def Pos.next? {s : String} (pos : s.Pos) : Option s.Pos :=
|
||||
pos.toSlice.next?.map Slice.Pos.ofSlice
|
||||
pos.toSlice.next?.map Pos.ofToSlice
|
||||
|
||||
/-- Advances a valid position on a string to the next valid position, or panics if the given
|
||||
position is the past-the-end position. -/
|
||||
@[inline, expose]
|
||||
def Pos.next! {s : String} (pos : s.Pos) : s.Pos :=
|
||||
pos.toSlice.next!.ofSlice
|
||||
ofToSlice pos.toSlice.next!
|
||||
|
||||
/-- Returns the previous valid position before the given position, given a proof that the position
|
||||
is not the start position, which guarantees that such a position exists. -/
|
||||
@[inline, expose]
|
||||
def Pos.prev {s : String} (pos : s.Pos) (h : pos ≠ s.startPos) : s.Pos :=
|
||||
(pos.toSlice.prev (ne_of_apply_ne Slice.Pos.ofSlice (by simpa))).ofSlice
|
||||
ofToSlice (pos.toSlice.prev (ne_of_apply_ne Pos.ofToSlice (by simpa)))
|
||||
|
||||
/-- Returns the previous valid position before the given position, or `none` if the position is
|
||||
the start position. -/
|
||||
@[inline, expose]
|
||||
def Pos.prev? {s : String} (pos : s.Pos) : Option s.Pos :=
|
||||
pos.toSlice.prev?.map Slice.Pos.ofSlice
|
||||
pos.toSlice.prev?.map Pos.ofToSlice
|
||||
|
||||
/-- Returns the previous valid position before the given position, or panics if the position is
|
||||
the start position. -/
|
||||
@[inline, expose]
|
||||
def Pos.prev! {s : String} (pos : s.Pos) : s.Pos :=
|
||||
pos.toSlice.prev!.ofSlice
|
||||
ofToSlice pos.toSlice.prev!
|
||||
|
||||
/-- Constructs a valid position on `s` from a position and a proof that it is valid. -/
|
||||
@[inline, expose]
|
||||
def pos (s : String) (off : Pos.Raw) (h : off.IsValid s) : s.Pos :=
|
||||
(s.toSlice.pos off h.toSlice).ofSlice
|
||||
Pos.ofToSlice (s.toSlice.pos off h.toSlice)
|
||||
|
||||
/-- Constructs a valid position on `s` from a position, returning `none` if the position is not valid. -/
|
||||
@[inline, expose]
|
||||
def pos? (s : String) (off : Pos.Raw) : Option s.Pos :=
|
||||
(s.toSlice.pos? off).map Slice.Pos.ofSlice
|
||||
(s.toSlice.pos? off).map Pos.ofToSlice
|
||||
|
||||
/-- Constructs a valid position `s` from a position, panicking if the position is not valid. -/
|
||||
@[inline, expose]
|
||||
def pos! (s : String) (off : Pos.Raw) : s.Pos :=
|
||||
(s.toSlice.pos! off).ofSlice
|
||||
Pos.ofToSlice (s.toSlice.pos! off)
|
||||
|
||||
@[simp]
|
||||
theorem offset_pos {s : String} {off : Pos.Raw} {h} : (s.pos off h).offset = off := rfl
|
||||
|
|
@ -1814,10 +1810,10 @@ theorem Slice.Pos.prev_ne_endPos {s : Slice} {p : s.Pos} {h} : p.prev h ≠ s.en
|
|||
|
||||
@[simp]
|
||||
theorem Pos.prev_ne_endPos {s : String} {p : s.Pos} {h} : p.prev h ≠ s.endPos :=
|
||||
mt (congrArg (·.toSlice)) (Slice.Pos.prev_ne_endPos (h := mt (congrArg (·.ofSlice)) h))
|
||||
mt (congrArg (·.toSlice)) (Slice.Pos.prev_ne_endPos (h := mt (congrArg Pos.ofToSlice) (by simpa)))
|
||||
|
||||
theorem Pos.toSlice_prev {s : String} {p : s.Pos} {h} :
|
||||
(p.prev h).toSlice = p.toSlice.prev (ne_of_apply_ne Slice.Pos.ofSlice (by simpa)) := by
|
||||
(p.prev h).toSlice = p.toSlice.prev (ne_of_apply_ne Pos.ofToSlice (by simpa)) := by
|
||||
simp [prev]
|
||||
|
||||
theorem Slice.Pos.offset_prev_lt_offset {s : Slice} {p : s.Pos} {h} : (p.prev h).offset < p.offset := by
|
||||
|
|
@ -1936,7 +1932,7 @@ theorem Pos.get_toSlice {s : String} {p : s.Pos} {h} :
|
|||
rfl
|
||||
|
||||
theorem Pos.get_eq_get_toSlice {s : String} {p : s.Pos} {h} :
|
||||
p.get h = p.toSlice.get (ne_of_apply_ne Slice.Pos.ofSlice (by simp [h])) := rfl
|
||||
p.get h = p.toSlice.get (ne_of_apply_ne Pos.ofToSlice (by simp [h])) := rfl
|
||||
|
||||
@[simp]
|
||||
theorem Pos.offset_next {s : String} (p : s.Pos) (h : p ≠ s.endPos) :
|
||||
|
|
@ -1948,7 +1944,7 @@ theorem Pos.byteIdx_offset_next {s : String} (p : s.Pos) (h : p ≠ s.endPos) :
|
|||
simp
|
||||
|
||||
theorem Pos.toSlice_next {s : String} {p : s.Pos} {h} :
|
||||
(p.next h).toSlice = p.toSlice.next (ne_of_apply_ne Slice.Pos.ofSlice (by simpa)) := by
|
||||
(p.next h).toSlice = p.toSlice.next (ne_of_apply_ne Pos.ofToSlice (by simpa)) := by
|
||||
simp [next]
|
||||
|
||||
theorem Pos.byteIdx_lt_utf8ByteSize {s : String} (p : s.Pos) (h : p ≠ s.endPos) :
|
||||
|
|
@ -2052,15 +2048,15 @@ theorem Slice.Pos.next_le_of_lt {s : Slice} {p q : s.Pos} {h} : p < q → p.next
|
|||
· have := (p.next h).str.isValid.le_utf8ByteSize
|
||||
simpa [Nat.add_assoc] using this
|
||||
|
||||
theorem Slice.Pos.ofSlice_le_iff {s : String} {p : s.toSlice.Pos} {q : s.Pos} :
|
||||
p.ofSlice ≤ q ↔ p ≤ q.toSlice := Iff.rfl
|
||||
theorem Pos.ofToSlice_le_iff {s : String} {p : s.toSlice.Pos} {q : s.Pos} :
|
||||
ofToSlice p ≤ q ↔ p ≤ q.toSlice := Iff.rfl
|
||||
|
||||
@[simp]
|
||||
theorem Pos.toSlice_lt_toSlice_iff {s : String} {p q : s.Pos} :
|
||||
p.toSlice < q.toSlice ↔ p < q := Iff.rfl
|
||||
|
||||
theorem Pos.next_le_of_lt {s : String} {p q : s.Pos} {h} : p < q → p.next h ≤ q := by
|
||||
rw [next, Slice.Pos.ofSlice_le_iff, ← Pos.toSlice_lt_toSlice_iff]
|
||||
rw [next, Pos.ofToSlice_le_iff, ← Pos.toSlice_lt_toSlice_iff]
|
||||
exact Slice.Pos.next_le_of_lt
|
||||
|
||||
theorem Slice.Pos.get_eq_get_str {s : Slice} {p : s.Pos} {h} :
|
||||
|
|
@ -2159,11 +2155,8 @@ This happens to be equivalent to the constructor of `String.Slice`.
|
|||
-/
|
||||
@[inline, expose] -- For the defeq `(s.slice p₁ p₂).str = s`
|
||||
def slice (s : String) (startInclusive endExclusive : s.Pos)
|
||||
(h : startInclusive ≤ endExclusive) : String.Slice where
|
||||
str := s
|
||||
startInclusive
|
||||
endExclusive
|
||||
startInclusive_le_endExclusive := h
|
||||
(h : startInclusive ≤ endExclusive) : String.Slice :=
|
||||
s.toSlice.slice startInclusive.toSlice endExclusive.toSlice (by simpa)
|
||||
|
||||
@[simp]
|
||||
theorem str_slice {s : String} {startInclusive endExclusive h} :
|
||||
|
|
@ -2171,11 +2164,13 @@ theorem str_slice {s : String} {startInclusive endExclusive h} :
|
|||
|
||||
@[simp]
|
||||
theorem startInclusive_slice {s : String} {startInclusive endExclusive h} :
|
||||
(s.slice startInclusive endExclusive h).startInclusive = startInclusive := rfl
|
||||
(s.slice startInclusive endExclusive h).startInclusive = startInclusive := by
|
||||
simp [slice]
|
||||
|
||||
@[simp]
|
||||
theorem endExclusive_slice {s : String} {startInclusive endExclusive h} :
|
||||
(s.slice startInclusive endExclusive h).endExclusive = endExclusive := rfl
|
||||
(s.slice startInclusive endExclusive h).endExclusive = endExclusive := by
|
||||
simp [slice]
|
||||
|
||||
/-- Given a string and two valid positions within the string, obtain a slice on the string formed
|
||||
by the new bounds, or return `none` if the given end is strictly less then the given start. -/
|
||||
|
|
@ -2311,6 +2306,127 @@ def Pos.toReplaceEnd {s : String} (p₀ : s.Pos) (pos : s.Pos) (h : pos ≤ p₀
|
|||
theorem Pos.offset_sliceTo {s : String} {p₀ : s.Pos} {pos : s.Pos} {h : pos ≤ p₀} :
|
||||
(sliceTo p₀ pos h).offset = pos.offset := (rfl)
|
||||
|
||||
theorem Pos.Raw.isValidForSlice_slice {s : Slice} {p₀ p₁ : s.Pos} {h} (pos : Pos.Raw) :
|
||||
pos.IsValidForSlice (s.slice p₀ p₁ h) ↔
|
||||
pos.offsetBy p₀.offset ≤ p₁.offset ∧ (pos.offsetBy p₀.offset).IsValidForSlice s := by
|
||||
refine ⟨fun ⟨h₁, h₂⟩ => ?_, fun ⟨h₁, h₂⟩ => ⟨?_, ?_⟩⟩
|
||||
· have : pos.offsetBy p₀.offset ≤ p₁.offset := by
|
||||
simp [Slice.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at h h₁ ⊢
|
||||
omega
|
||||
exact ⟨this, ⟨Pos.Raw.le_trans this p₁.isValidForSlice.le_rawEndPos, by simpa [offsetBy_assoc]⟩⟩
|
||||
· simp [Slice.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at h h₁ ⊢
|
||||
omega
|
||||
· simpa [offsetBy_assoc] using h₂.isValid_offsetBy
|
||||
|
||||
theorem Pos.Raw.isValidForSlice_stringSlice {s : String} {p₀ p₁ : s.Pos} {h} (pos : Pos.Raw) :
|
||||
pos.IsValidForSlice (s.slice p₀ p₁ h) ↔
|
||||
pos.offsetBy p₀.offset ≤ p₁.offset ∧ (pos.offsetBy p₀.offset).IsValid s := by
|
||||
simp [slice, isValidForSlice_slice]
|
||||
|
||||
/-- Given a position in `s.slice p₀ p₁ h`, obtain the corresponding position in `s`. -/
|
||||
@[inline]
|
||||
def Slice.Pos.ofSlice {s : Slice} {p₀ p₁ : s.Pos} {h} (pos : (s.slice p₀ p₁ h).Pos) : s.Pos where
|
||||
offset := pos.offset.offsetBy p₀.offset
|
||||
isValidForSlice := (Pos.Raw.isValidForSlice_slice _).1 pos.isValidForSlice |>.2
|
||||
@[simp]
|
||||
theorem Slice.Pos.offset_ofSlice {s : Slice} {p₀ p₁ : s.Pos} {h} {pos : (s.slice p₀ p₁ h).Pos} :
|
||||
(Pos.ofSlice pos).offset = pos.offset.offsetBy p₀.offset := (rfl)
|
||||
|
||||
/-- Given a position in `s.slice p₀ p₁ h`, obtain the corresponding position in `s`. -/
|
||||
@[inline]
|
||||
def Pos.ofSlice {s : String} {p₀ p₁ : s.Pos} {h} (pos : (s.slice p₀ p₁ h).Pos) : s.Pos :=
|
||||
ofToSlice (Slice.Pos.ofSlice pos)
|
||||
|
||||
@[simp]
|
||||
theorem Pos.offset_ofSlice {s : String} {p₀ p₁ : s.Pos} {h} {pos : (s.slice p₀ p₁ h).Pos} :
|
||||
(Pos.ofSlice pos).offset = pos.offset.offsetBy p₀.offset := (rfl)
|
||||
|
||||
theorem Slice.Pos.le_trans {s : Slice} {p q r : s.Pos} : p ≤ q → q ≤ r → p ≤ r := by
|
||||
simpa [Pos.le_iff, Pos.Raw.le_iff] using Nat.le_trans
|
||||
|
||||
/-- Given a position in `s` that is between `p₀` and `p₁`, obtain the corresponding position in
|
||||
`s.slice p₀ p₁ h`. -/
|
||||
@[inline]
|
||||
def Slice.Pos.slice {s : Slice} (pos : s.Pos) (p₀ p₁ : s.Pos) (h₁ : p₀ ≤ pos) (h₂ : pos ≤ p₁) :
|
||||
(s.slice p₀ p₁ (Slice.Pos.le_trans h₁ h₂)).Pos where
|
||||
offset := pos.offset.unoffsetBy p₀.offset
|
||||
isValidForSlice := (Pos.Raw.isValidForSlice_slice _).2
|
||||
(by simp [Pos.Raw.offsetBy_unoffsetBy_of_le h₁, Slice.Pos.le_iff.1 h₂, pos.isValidForSlice])
|
||||
|
||||
/-- Given a position in `s` that is between `p₀` and `p₁`, obtain the corresponding position in
|
||||
`s.slice p₀ p₁ h`. -/
|
||||
@[inline]
|
||||
def Pos.slice {s : String} (pos : s.Pos) (p₀ p₁ : s.Pos) (h₁ : p₀ ≤ pos) (h₂ : pos ≤ p₁) :
|
||||
(s.slice p₀ p₁ (Pos.le_trans h₁ h₂)).Pos :=
|
||||
Slice.Pos.slice pos.toSlice _ _ h₁ h₂
|
||||
|
||||
@[simp]
|
||||
theorem Pos.offset_slice {s : String} {p₀ p₁ pos : s.Pos} {h₁ : p₀ ≤ pos} {h₂ : pos ≤ p₁} :
|
||||
(pos.slice p₀ p₁ h₁ h₂).offset = pos.offset.unoffsetBy p₀.offset := (rfl)
|
||||
|
||||
/--
|
||||
Given a position in `s`, obtain the corresponding position in `s.slice p₀ p₁ h`, or panic if `pos`
|
||||
is not between `p₀` and `p₁`.
|
||||
-/
|
||||
@[inline]
|
||||
def Slice.Pos.sliceOrPanic {s : Slice} (pos : s.Pos) (p₀ p₁ : s.Pos) {h} :
|
||||
(s.slice p₀ p₁ h).Pos :=
|
||||
if h : p₀ ≤ pos ∧ pos ≤ p₁ then
|
||||
pos.slice p₀ p₁ h.1 h.2
|
||||
else
|
||||
panic! "Position is outside of the bounds of the slice."
|
||||
|
||||
/--
|
||||
Given a position in `s`, obtain the corresponding position in `s.slice p₀ p₁ h`, or panic if `pos`
|
||||
is not between `p₀` and `p₁`.
|
||||
-/
|
||||
@[inline]
|
||||
def Pos.sliceOrPanic {s : String} (pos : s.Pos) (p₀ p₁ : s.Pos) {h} :
|
||||
(s.slice p₀ p₁ h).Pos :=
|
||||
Slice.Pos.sliceOrPanic pos.toSlice _ _
|
||||
|
||||
theorem Slice.slice_eq_slice! {s : Slice} {p₀ p₁ h} : s.slice p₀ p₁ h = s.slice! p₀ p₁ := by
|
||||
simp [slice!, h]
|
||||
|
||||
theorem slice_eq_slice! {s : String} {p₀ p₁ h} : s.slice p₀ p₁ h = s.slice! p₀ p₁ := by
|
||||
simp [slice!, slice, Slice.slice_eq_slice!]
|
||||
|
||||
/-- Given a position in `s.slice! p₀ p₁`, obtain the corresponding position in `s`, or panic if
|
||||
taking `s.slice! p₀ p₁` already panicked. -/
|
||||
@[inline]
|
||||
def Slice.Pos.ofSlice! {s : Slice} {p₀ p₁ : s.Pos} (pos : (s.slice! p₀ p₁).Pos) : s.Pos :=
|
||||
if h : p₀ ≤ p₁ then
|
||||
ofSlice (h := h) (pos.cast slice_eq_slice!.symm)
|
||||
else
|
||||
panic! "Starting position must be less than or equal to end position."
|
||||
|
||||
/-- Given a position in `s.slice! p₀ p₁`, obtain the corresponding position in `s`, or panic if
|
||||
taking `s.slice! p₀ p₁` already panicked. -/
|
||||
@[inline]
|
||||
def Pos.ofSlice! {s : String} {p₀ p₁ : s.Pos} (pos : (s.slice! p₀ p₁).Pos) : s.Pos :=
|
||||
ofToSlice (Slice.Pos.ofSlice! pos)
|
||||
|
||||
/--
|
||||
Given a position in `s`, obtain the corresponding position in `s.slice! p₀ p₁ h`, or panic if
|
||||
taking `s.slice! p₀ p₁` already panicked or if the position is not between `p₀` and `p₁`.
|
||||
-/
|
||||
@[inline]
|
||||
def Slice.Pos.slice! {s : Slice} (pos : s.Pos) (p₀ p₁ : s.Pos) :
|
||||
(s.slice! p₀ p₁).Pos :=
|
||||
if h : p₀ ≤ pos ∧ pos ≤ p₁ then
|
||||
(pos.slice _ _ h.1 h.2).cast slice_eq_slice!
|
||||
else
|
||||
panic! "Starting position must be less than or equal to end position and position must be between starting position and end position."
|
||||
|
||||
/--
|
||||
Given a position in `s`, obtain the corresponding position in `s.slice! p₀ p₁ h`, or panic if
|
||||
taking `s.slice! p₀ p₁` already panicked or if the position is not between `p₀` and `p₁`.
|
||||
-/
|
||||
@[inline]
|
||||
def Pos.slice! {s : String} (pos : s.Pos) (p₀ p₁ : s.Pos) :
|
||||
(s.slice! p₀ p₁).Pos :=
|
||||
Slice.Pos.slice! pos.toSlice _ _
|
||||
|
||||
/--
|
||||
Advances the position `p` `n` times.
|
||||
|
||||
|
|
@ -2346,7 +2462,7 @@ If this would move `p` past the end of `s`, the result is `s.endPos`.
|
|||
-/
|
||||
@[inline]
|
||||
def Pos.nextn {s : String} (p : s.Pos) (n : Nat) : s.Pos :=
|
||||
(p.toSlice.nextn n).ofSlice
|
||||
ofToSlice (p.toSlice.nextn n)
|
||||
|
||||
/--
|
||||
Iterates `p.prev` `n` times.
|
||||
|
|
@ -2355,7 +2471,7 @@ If this would move `p` past the start of `s`, the result is `s.startPos`.
|
|||
-/
|
||||
@[inline]
|
||||
def Pos.prevn {s : String} (p : s.Pos) (n : Nat) : s.Pos :=
|
||||
(p.toSlice.prevn n).ofSlice
|
||||
ofToSlice (p.toSlice.prevn n)
|
||||
|
||||
theorem Slice.Pos.le_nextn {s : Slice} {p : s.Pos} {n : Nat} : p ≤ p.nextn n := by
|
||||
fun_induction nextn with
|
||||
|
|
|
|||
|
|
@ -94,7 +94,7 @@ Examples:
|
|||
@[inline]
|
||||
def Pos.find? {s : String} (pos : s.Pos) (pattern : ρ)
|
||||
[ToForwardSearcher pattern σ] : Option s.Pos :=
|
||||
(pos.toSlice.find? pattern).map (·.ofSlice)
|
||||
(pos.toSlice.find? pattern).map Pos.ofToSlice
|
||||
|
||||
/--
|
||||
Finds the position of the first match of the pattern {name}`pattern` in after the position
|
||||
|
|
@ -109,7 +109,7 @@ Examples:
|
|||
@[inline]
|
||||
def Pos.find {s : String} (pos : s.Pos) (pattern : ρ) [ToForwardSearcher pattern σ] :
|
||||
s.Pos :=
|
||||
(pos.toSlice.find pattern).ofSlice
|
||||
ofToSlice (pos.toSlice.find pattern)
|
||||
|
||||
/--
|
||||
Finds the position of the first match of the pattern {name}`pattern` in a string {name}`s`. If
|
||||
|
|
@ -172,7 +172,7 @@ Examples:
|
|||
@[inline]
|
||||
def Pos.revFind? {s : String} (pos : s.Pos) (pattern : ρ) [ToBackwardSearcher pattern σ] :
|
||||
Option s.Pos :=
|
||||
(pos.toSlice.revFind? pattern).map (·.ofSlice)
|
||||
(pos.toSlice.revFind? pattern).map Pos.ofToSlice
|
||||
|
||||
/--
|
||||
Finds the position of the first match of the pattern {name}`pattern` in a string, starting
|
||||
|
|
@ -539,14 +539,14 @@ Examples:
|
|||
@[inline, expose] def back (s : String) : Char :=
|
||||
s.toSlice.back
|
||||
|
||||
theorem Slice.Pos.ofSlice_ne_endPos {s : String} {p : s.toSlice.Pos}
|
||||
(h : p ≠ s.toSlice.endPos) : p.ofSlice ≠ s.endPos := by
|
||||
rwa [ne_eq, ← Pos.toSlice_inj, toSlice_ofSlice, ← endPos_toSlice]
|
||||
theorem Pos.ofToSlice_ne_endPos {s : String} {p : s.toSlice.Pos}
|
||||
(h : p ≠ s.toSlice.endPos) : ofToSlice p ≠ s.endPos := by
|
||||
rwa [ne_eq, ← Pos.toSlice_inj, Slice.Pos.toSlice_ofToSlice, ← endPos_toSlice]
|
||||
|
||||
@[inline]
|
||||
def Internal.toSliceWithProof {s : String} :
|
||||
{ p : s.toSlice.Pos // p ≠ s.toSlice.endPos } → { p : s.Pos // p ≠ s.endPos } :=
|
||||
fun ⟨p, h⟩ => ⟨p.ofSlice, Slice.Pos.ofSlice_ne_endPos h⟩
|
||||
fun ⟨p, h⟩ => ⟨Pos.ofToSlice p, Pos.ofToSlice_ne_endPos h⟩
|
||||
|
||||
/--
|
||||
Creates an iterator over all valid positions within {name}`s`.
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue