From 0f730662de0bbaa6ed07484d8f0e411de2bcd1ea Mon Sep 17 00:00:00 2001 From: Markus Himmel <2065352+TwoFX@users.noreply.github.com> Date: Thu, 19 Mar 2026 16:45:53 +0100 Subject: [PATCH] refactor: reorganize functions for skipping/dropping prefixes/suffixes of strings (#12988) This PR introduces the functions `String.Slice.skipPrefix?`, `String.Slice.Pos.skip?`, `String.Slice.skipPrefixWhile`, `String.Slice.Pos.skipWhile` and redefines `String.Slice.takeWhile` and `String.Slice.dropWhile` to use these new functions. --- src/Init/Data/String/Lemmas/Pattern/Char.lean | 82 +++++----- src/Init/Data/String/Lemmas/Pattern/Pred.lean | 88 +++++------ .../Lemmas/Pattern/String/ForwardPattern.lean | 84 +++++------ src/Init/Data/String/Pattern/Basic.lean | 26 ++-- src/Init/Data/String/Pattern/Char.lean | 6 +- src/Init/Data/String/Pattern/Pred.lean | 18 +-- src/Init/Data/String/Pattern/String.lean | 6 +- src/Init/Data/String/Slice.lean | 140 +++++++++++------- src/Init/Data/String/TakeDrop.lean | 66 +++++++++ 9 files changed, 295 insertions(+), 221 deletions(-) diff --git a/src/Init/Data/String/Lemmas/Pattern/Char.lean b/src/Init/Data/String/Lemmas/Pattern/Char.lean index fb3b60c7c8..f7ba076400 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Char.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Char.lean @@ -136,42 +136,36 @@ theorem dropPrefix?_char_eq_dropPrefix?_beq {c : Char} {s : Slice} : theorem dropPrefix_char_eq_dropPrefix_beq {c : Char} {s : Slice} : s.dropPrefix c = s.dropPrefix (· == c) := (rfl) +theorem skipPrefix?_char_eq_skipPrefix?_beq {c : Char} {s : Slice} : + s.skipPrefix? c = s.skipPrefix? (· == c) := (rfl) + theorem Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq {c : Char} {s : Slice} : skipPrefix? c s = skipPrefix? (· == c) s := (rfl) -private theorem dropWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) : - dropWhile.go s c curr = dropWhile.go s (· == c) curr := by - fun_induction dropWhile.go s c curr with +theorem Pos.skipWhile_char_eq_skipWhile_beq {c : Char} {s : Slice} (curr : s.Pos) : + Pos.skipWhile curr c = Pos.skipWhile curr (· == c) := by + fun_induction Pos.skipWhile curr c with | case1 pos nextCurr h₁ h₂ ih => - conv => rhs; rw [dropWhile.go] + conv => rhs; rw [Pos.skipWhile] simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h₁, h₂, ih] | case2 pos nextCurr h ih => - conv => rhs; rw [dropWhile.go] + conv => rhs; rw [Pos.skipWhile] simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h, ih] | case3 pos h => - conv => rhs; rw [dropWhile.go] + conv => rhs; rw [Pos.skipWhile] simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq] +theorem skipPrefixWhile_char_eq_skipPrefixWhile_beq {c : Char} {s : Slice} : + s.skipPrefixWhile c = s.skipPrefixWhile (· == c) := + Pos.skipWhile_char_eq_skipWhile_beq s.startPos + theorem dropWhile_char_eq_dropWhile_beq {c : Char} {s : Slice} : s.dropWhile c = s.dropWhile (· == c) := by - simpa only [dropWhile] using dropWhileGo_eq s.startPos - -private theorem takeWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) : - takeWhile.go s c curr = takeWhile.go s (· == c) curr := by - fun_induction takeWhile.go s c curr with - | case1 pos nextCurr h₁ h₂ ih => - conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h₁, h₂, ih] - | case2 pos nextCurr h ih => - conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h, ih] - | case3 pos h => - conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq] + simp only [dropWhile]; exact congrArg _ skipPrefixWhile_char_eq_skipPrefixWhile_beq theorem takeWhile_char_eq_takeWhile_beq {c : Char} {s : Slice} : s.takeWhile c = s.takeWhile (· == c) := by - simp only [takeWhile]; exact takeWhileGo_eq s.startPos + simp only [takeWhile]; exact congrArg _ skipPrefixWhile_char_eq_skipPrefixWhile_beq theorem all_char_eq_all_beq {c : Char} {s : Slice} : s.all c = s.all (· == c) := by @@ -192,47 +186,41 @@ theorem contains_char_eq_contains_beq {c : Char} {s : Slice} : theorem endsWith_char_eq_endsWith_beq {c : Char} {s : Slice} : s.endsWith c = s.endsWith (· == c) := (rfl) +theorem skipSuffix?_char_eq_skipSuffix?_beq {c : Char} {s : Slice} : + s.skipSuffix? c = s.skipSuffix? (· == c) := (rfl) + theorem dropSuffix?_char_eq_dropSuffix?_beq {c : Char} {s : Slice} : s.dropSuffix? c = s.dropSuffix? (· == c) := (rfl) theorem dropSuffix_char_eq_dropSuffix_beq {c : Char} {s : Slice} : s.dropSuffix c = s.dropSuffix (· == c) := (rfl) -theorem Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq {c : Char} {s : Slice} : - dropSuffix? c s = dropSuffix? (· == c) s := (rfl) +theorem Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq {c : Char} {s : Slice} : + skipSuffix? c s = skipSuffix? (· == c) s := (rfl) -private theorem dropEndWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) : - dropEndWhile.go s c curr = dropEndWhile.go s (· == c) curr := by - fun_induction dropEndWhile.go s c curr with +theorem Pos.revSkipWhile_char_eq_revSkipWhile_beq {c : Char} {s : Slice} (curr : s.Pos) : + Pos.revSkipWhile curr c = Pos.revSkipWhile curr (· == c) := by + fun_induction Pos.revSkipWhile curr c with | case1 pos nextCurr h₁ h₂ ih => - conv => rhs; rw [dropEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h₁, h₂, ih] + conv => rhs; rw [Pos.revSkipWhile] + simp [← Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq, h₁, h₂, ih] | case2 pos nextCurr h ih => - conv => rhs; rw [dropEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h, ih] + conv => rhs; rw [Pos.revSkipWhile] + simp [← Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq, h, ih] | case3 pos h => - conv => rhs; rw [dropEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq] + conv => rhs; rw [Pos.revSkipWhile] + simp [← Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq] + +theorem skipSuffixWhile_char_eq_skipSuffixWhile_beq {c : Char} {s : Slice} : + s.skipSuffixWhile c = s.skipSuffixWhile (· == c) := + Pos.revSkipWhile_char_eq_revSkipWhile_beq s.endPos theorem dropEndWhile_char_eq_dropEndWhile_beq {c : Char} {s : Slice} : s.dropEndWhile c = s.dropEndWhile (· == c) := by - simpa only [dropEndWhile] using dropEndWhileGo_eq s.endPos - -private theorem takeEndWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) : - takeEndWhile.go s c curr = takeEndWhile.go s (· == c) curr := by - fun_induction takeEndWhile.go s c curr with - | case1 pos nextCurr h₁ h₂ ih => - conv => rhs; rw [takeEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h₁, h₂, ih] - | case2 pos nextCurr h ih => - conv => rhs; rw [takeEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h, ih] - | case3 pos h => - conv => rhs; rw [takeEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq] + simp only [dropEndWhile]; exact congrArg _ skipSuffixWhile_char_eq_skipSuffixWhile_beq theorem takeEndWhile_char_eq_takeEndWhile_beq {c : Char} {s : Slice} : s.takeEndWhile c = s.takeEndWhile (· == c) := by - simpa only [takeEndWhile] using takeEndWhileGo_eq s.endPos + simp only [takeEndWhile]; exact congrArg _ skipSuffixWhile_char_eq_skipSuffixWhile_beq end String.Slice diff --git a/src/Init/Data/String/Lemmas/Pattern/Pred.lean b/src/Init/Data/String/Lemmas/Pattern/Pred.lean index d55e8a92a9..163c0b3da1 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Pred.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Pred.lean @@ -181,43 +181,39 @@ theorem dropPrefix?_prop_eq_dropPrefix?_decide {p : Char → Prop} [DecidablePre theorem dropPrefix_prop_eq_dropPrefix_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.dropPrefix p = s.dropPrefix (decide <| p ·) := (rfl) +theorem skipPrefix?_prop_eq_skipPrefix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : + s.skipPrefix? p = s.skipPrefix? (decide <| p ·) := (rfl) + theorem Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : skipPrefix? p s = skipPrefix? (decide <| p ·) s := (rfl) -private theorem dropWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice} (curr : s.Pos) : - dropWhile.go s p curr = dropWhile.go s (decide <| p ·) curr := by - fun_induction dropWhile.go s p curr with +theorem Pos.skipWhile_prop_eq_skipWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} + (curr : s.Pos) : + Pos.skipWhile curr p = Pos.skipWhile curr (decide <| p ·) := by + fun_induction Pos.skipWhile curr p with | case1 pos nextCurr h₁ h₂ ih => - conv => rhs; rw [dropWhile.go] + conv => rhs; rw [Pos.skipWhile] simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h₁, h₂, ih] | case2 pos nextCurr h ih => - conv => rhs; rw [dropWhile.go] + conv => rhs; rw [Pos.skipWhile] simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h, ih] | case3 pos h => - conv => rhs; rw [dropWhile.go] + conv => rhs; rw [Pos.skipWhile] simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide] +theorem skipPrefixWhile_prop_eq_skipPrefixWhile_decide {p : Char → Prop} [DecidablePred p] + {s : Slice} : + s.skipPrefixWhile p = s.skipPrefixWhile (decide <| p ·) := + Pos.skipWhile_prop_eq_skipWhile_decide s.startPos + theorem dropWhile_prop_eq_dropWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.dropWhile p = s.dropWhile (decide <| p ·) := by - simpa only [dropWhile] using dropWhileGo_eq s.startPos - -private theorem takeWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice} (curr : s.Pos) : - takeWhile.go s p curr = takeWhile.go s (decide <| p ·) curr := by - fun_induction takeWhile.go s p curr with - | case1 pos nextCurr h₁ h₂ ih => - conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h₁, h₂, ih] - | case2 pos nextCurr h ih => - conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h, ih] - | case3 pos h => - conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide] + simp only [dropWhile]; exact congrArg _ skipPrefixWhile_prop_eq_skipPrefixWhile_decide theorem takeWhile_prop_eq_takeWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.takeWhile p = s.takeWhile (decide <| p ·) := by - simp only [takeWhile]; exact takeWhileGo_eq s.startPos + simp only [takeWhile]; exact congrArg _ skipPrefixWhile_prop_eq_skipPrefixWhile_decide theorem all_prop_eq_all_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.all p = s.all (decide <| p ·) := by @@ -239,52 +235,46 @@ theorem contains_prop_eq_contains_decide {p : Char → Prop} [DecidablePred p] { theorem endsWith_prop_eq_endsWith_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.endsWith p = s.endsWith (decide <| p ·) := (rfl) +theorem skipSuffix?_prop_eq_skipSuffix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : + s.skipSuffix? p = s.skipSuffix? (decide <| p ·) := (rfl) + theorem dropSuffix?_prop_eq_dropSuffix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.dropSuffix? p = s.dropSuffix? (decide <| p ·) := (rfl) theorem dropSuffix_prop_eq_dropSuffix_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.dropSuffix p = s.dropSuffix (decide <| p ·) := (rfl) -theorem Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide +theorem Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : - dropSuffix? p s = dropSuffix? (decide <| p ·) s := (rfl) + skipSuffix? p s = skipSuffix? (decide <| p ·) s := (rfl) -private theorem dropEndWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice} - (curr : s.Pos) : - dropEndWhile.go s p curr = dropEndWhile.go s (decide <| p ·) curr := by - fun_induction dropEndWhile.go s p curr with +theorem Pos.revSkipWhile_prop_eq_revSkipWhile_decide {p : Char → Prop} [DecidablePred p] + {s : Slice} (curr : s.Pos) : + Pos.revSkipWhile curr p = Pos.revSkipWhile curr (decide <| p ·) := by + fun_induction Pos.revSkipWhile curr p with | case1 pos nextCurr h₁ h₂ ih => - conv => rhs; rw [dropEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h₁, h₂, ih] + conv => rhs; rw [Pos.revSkipWhile] + simp [← Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide, h₁, h₂, ih] | case2 pos nextCurr h ih => - conv => rhs; rw [dropEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h, ih] + conv => rhs; rw [Pos.revSkipWhile] + simp [← Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide, h, ih] | case3 pos h => - conv => rhs; rw [dropEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide] + conv => rhs; rw [Pos.revSkipWhile] + simp [← Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide] + +theorem skipSuffixWhile_prop_eq_skipSuffixWhile_decide {p : Char → Prop} [DecidablePred p] + {s : Slice} : + s.skipSuffixWhile p = s.skipSuffixWhile (decide <| p ·) := + Pos.revSkipWhile_prop_eq_revSkipWhile_decide s.endPos theorem dropEndWhile_prop_eq_dropEndWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.dropEndWhile p = s.dropEndWhile (decide <| p ·) := by - simpa only [dropEndWhile] using dropEndWhileGo_eq s.endPos - -private theorem takeEndWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice} - (curr : s.Pos) : - takeEndWhile.go s p curr = takeEndWhile.go s (decide <| p ·) curr := by - fun_induction takeEndWhile.go s p curr with - | case1 pos nextCurr h₁ h₂ ih => - conv => rhs; rw [takeEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h₁, h₂, ih] - | case2 pos nextCurr h ih => - conv => rhs; rw [takeEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h, ih] - | case3 pos h => - conv => rhs; rw [takeEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide] + simp only [dropEndWhile]; exact congrArg _ skipSuffixWhile_prop_eq_skipSuffixWhile_decide theorem takeEndWhile_prop_eq_takeEndWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.takeEndWhile p = s.takeEndWhile (decide <| p ·) := by - simpa only [takeEndWhile] using takeEndWhileGo_eq s.endPos + simp only [takeEndWhile]; exact congrArg _ skipSuffixWhile_prop_eq_skipSuffixWhile_decide end String.Slice diff --git a/src/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.lean b/src/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.lean index 9f627cb836..9d0d71d36a 100644 --- a/src/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.lean +++ b/src/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.lean @@ -100,43 +100,38 @@ public theorem dropPrefix?_string_eq_dropPrefix?_toSlice {pat : String} {s : Sli public theorem dropPrefix_string_eq_dropPrefix_toSlice {pat : String} {s : Slice} : s.dropPrefix pat = s.dropPrefix pat.toSlice := (rfl) +public theorem skipPrefix?_string_eq_skipPrefix?_toSlice {pat : String} {s : Slice} : + s.skipPrefix? pat = s.skipPrefix? pat.toSlice := (rfl) + public theorem Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice {pat : String} {s : Slice} : skipPrefix? pat s = skipPrefix? pat.toSlice s := (rfl) -private theorem dropWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) : - dropWhile.go s pat curr = dropWhile.go s pat.toSlice curr := by - fun_induction dropWhile.go s pat curr with +public theorem Pos.skipWhile_string_eq_skipWhile_toSlice {pat : String} {s : Slice} + (curr : s.Pos) : + Pos.skipWhile curr pat = Pos.skipWhile curr pat.toSlice := by + fun_induction Pos.skipWhile curr pat with | case1 pos nextCurr h₁ h₂ ih => - conv => rhs; rw [dropWhile.go] + conv => rhs; rw [Pos.skipWhile] simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice, h₁, h₂, ih] | case2 pos nextCurr h ih => - conv => rhs; rw [dropWhile.go] + conv => rhs; rw [Pos.skipWhile] simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice, h, ih] | case3 pos h => - conv => rhs; rw [dropWhile.go] + conv => rhs; rw [Pos.skipWhile] simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice] +public theorem skipPrefixWhile_string_eq_skipPrefixWhile_toSlice {pat : String} {s : Slice} : + s.skipPrefixWhile pat = s.skipPrefixWhile pat.toSlice := + Pos.skipWhile_string_eq_skipWhile_toSlice s.startPos + public theorem dropWhile_string_eq_dropWhile_toSlice {pat : String} {s : Slice} : s.dropWhile pat = s.dropWhile pat.toSlice := by - simpa only [dropWhile] using dropWhileGo_string_eq s.startPos - -private theorem takeWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) : - takeWhile.go s pat curr = takeWhile.go s pat.toSlice curr := by - fun_induction takeWhile.go s pat curr with - | case1 pos nextCurr h₁ h₂ ih => - conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice, h₁, h₂, ih] - | case2 pos nextCurr h ih => - conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice, h, ih] - | case3 pos h => - conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice] + simp only [dropWhile]; exact congrArg _ skipPrefixWhile_string_eq_skipPrefixWhile_toSlice public theorem takeWhile_string_eq_takeWhile_toSlice {pat : String} {s : Slice} : s.takeWhile pat = s.takeWhile pat.toSlice := by - simp only [takeWhile]; exact takeWhileGo_string_eq s.startPos + simp only [takeWhile]; exact congrArg _ skipPrefixWhile_string_eq_skipPrefixWhile_toSlice public theorem all_string_eq_all_toSlice {pat : String} {s : Slice} : s.all pat = s.all pat.toSlice := by @@ -145,48 +140,43 @@ public theorem all_string_eq_all_toSlice {pat : String} {s : Slice} : public theorem endsWith_string_eq_endsWith_toSlice {pat : String} {s : Slice} : s.endsWith pat = s.endsWith pat.toSlice := (rfl) +public theorem skipSuffix?_string_eq_skipSuffix?_toSlice {pat : String} {s : Slice} : + s.skipSuffix? pat = s.skipSuffix? pat.toSlice := (rfl) + public theorem dropSuffix?_string_eq_dropSuffix?_toSlice {pat : String} {s : Slice} : s.dropSuffix? pat = s.dropSuffix? pat.toSlice := (rfl) public theorem dropSuffix_string_eq_dropSuffix_toSlice {pat : String} {s : Slice} : s.dropSuffix pat = s.dropSuffix pat.toSlice := (rfl) -public theorem Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice +public theorem Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice {pat : String} {s : Slice} : - dropSuffix? pat s = dropSuffix? pat.toSlice s := (rfl) + skipSuffix? pat s = skipSuffix? pat.toSlice s := (rfl) -private theorem dropEndWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) : - dropEndWhile.go s pat curr = dropEndWhile.go s pat.toSlice curr := by - fun_induction dropEndWhile.go s pat curr with +public theorem Pos.revSkipWhile_string_eq_revSkipWhile_toSlice {pat : String} {s : Slice} + (curr : s.Pos) : + Pos.revSkipWhile curr pat = Pos.revSkipWhile curr pat.toSlice := by + fun_induction Pos.revSkipWhile curr pat with | case1 pos nextCurr h₁ h₂ ih => - conv => rhs; rw [dropEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h₁, h₂, ih] + conv => rhs; rw [Pos.revSkipWhile] + simp [← Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice, h₁, h₂, ih] | case2 pos nextCurr h ih => - conv => rhs; rw [dropEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h, ih] + conv => rhs; rw [Pos.revSkipWhile] + simp [← Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice, h, ih] | case3 pos h => - conv => rhs; rw [dropEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice] + conv => rhs; rw [Pos.revSkipWhile] + simp [← Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice] + +public theorem skipSuffixWhile_string_eq_skipSuffixWhile_toSlice {pat : String} {s : Slice} : + s.skipSuffixWhile pat = s.skipSuffixWhile pat.toSlice := + Pos.revSkipWhile_string_eq_revSkipWhile_toSlice s.endPos public theorem dropEndWhile_string_eq_dropEndWhile_toSlice {pat : String} {s : Slice} : s.dropEndWhile pat = s.dropEndWhile pat.toSlice := by - simpa only [dropEndWhile] using dropEndWhileGo_string_eq s.endPos - -private theorem takeEndWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) : - takeEndWhile.go s pat curr = takeEndWhile.go s pat.toSlice curr := by - fun_induction takeEndWhile.go s pat curr with - | case1 pos nextCurr h₁ h₂ ih => - conv => rhs; rw [takeEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h₁, h₂, ih] - | case2 pos nextCurr h ih => - conv => rhs; rw [takeEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h, ih] - | case3 pos h => - conv => rhs; rw [takeEndWhile.go] - simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice] + simp only [dropEndWhile]; exact congrArg _ skipSuffixWhile_string_eq_skipSuffixWhile_toSlice public theorem takeEndWhile_string_eq_takeEndWhile_toSlice {pat : String} {s : Slice} : s.takeEndWhile pat = s.takeEndWhile pat.toSlice := by - simpa only [takeEndWhile] using takeEndWhileGo_string_eq s.endPos + simp only [takeEndWhile]; exact congrArg _ skipSuffixWhile_string_eq_skipSuffixWhile_toSlice end String.Slice diff --git a/src/Init/Data/String/Pattern/Basic.lean b/src/Init/Data/String/Pattern/Basic.lean index 68a2211438..021f585f0b 100644 --- a/src/Init/Data/String/Pattern/Basic.lean +++ b/src/Init/Data/String/Pattern/Basic.lean @@ -316,20 +316,20 @@ 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 + skipSuffix? : (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 + skipSuffixOfNonempty? : (s : Slice) → (h : s.isEmpty = false) → Option s.Pos := fun s _ => skipSuffix? s /-- Checks whether the slice ends with the pattern. -/ - endsWith : Slice → Bool := fun s => (dropSuffix? s).isSome + endsWith : Slice → Bool := fun s => (skipSuffix? s).isSome /-- -A lawful backward pattern is one where the three functions {name}`BackwardPattern.dropSuffix?`, -{name}`BackwardPattern.dropSuffixOfNonempty?` and {name}`BackwardPattern.endsWith` agree for any +A lawful backward pattern is one where the three functions {name}`BackwardPattern.skipSuffix?`, +{name}`BackwardPattern.skipSuffixOfNonempty?` and {name}`BackwardPattern.endsWith` agree for any given input slice. Note that this is a relatively weak condition. It is non-uniform in the sense that the functions @@ -337,14 +337,14 @@ can still return completely different results on different slices, even if they string. 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 +{name}`BackwardPattern.skipSuffix?` function behaves like a function that skips 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 + skipSuffixOfNonempty?_eq {s : Slice} (h) : + BackwardPattern.skipSuffixOfNonempty? pat s h = BackwardPattern.skipSuffix? pat s endsWith_eq (s : Slice) : - BackwardPattern.endsWith pat s = (BackwardPattern.dropSuffix? pat s).isSome + BackwardPattern.endsWith pat s = (BackwardPattern.skipSuffix? pat s).isSome /-- A strict backward pattern is one which never drops an empty suffix. @@ -354,7 +354,7 @@ 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 + BackwardPattern.skipSuffixOfNonempty? pat s h = some q → q ≠ s.endPos /-- Provides a conversion from a pattern to an iterator of {name}`SearchStep` searching for matches of @@ -398,11 +398,11 @@ 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 ∧ + BackwardPattern.skipSuffixOfNonempty? 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 ∧ + BackwardPattern.skipSuffixOfNonempty? 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 @@ -411,7 +411,7 @@ instance (s : Slice) [BackwardPattern pat] : 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 + match h' : BackwardPattern.skipSuffixOfNonempty? 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']⟩) diff --git a/src/Init/Data/String/Pattern/Char.lean b/src/Init/Data/String/Pattern/Char.lean index 26eee1ab2e..eb8276e01d 100644 --- a/src/Init/Data/String/Pattern/Char.lean +++ b/src/Init/Data/String/Pattern/Char.lean @@ -36,15 +36,15 @@ instance {c : Char} : ToForwardSearcher c (ToForwardSearcher.DefaultForwardSearc toSearcher s := ToForwardSearcher.toSearcher (· == c) s instance {c : Char} : BackwardPattern c where - dropSuffixOfNonempty? s h := BackwardPattern.dropSuffixOfNonempty? (· == c) s h - dropSuffix? s := BackwardPattern.dropSuffix? (· == c) s + skipSuffixOfNonempty? s h := BackwardPattern.skipSuffixOfNonempty? (· == c) s h + skipSuffix? s := BackwardPattern.skipSuffix? (· == c) s endsWith s := BackwardPattern.endsWith (· == c) s instance {c : Char} : StrictBackwardPattern c where ne_endPos h q := StrictBackwardPattern.ne_endPos (pat := (· == c)) h q instance {c : Char} : LawfulBackwardPattern c where - dropSuffixOfNonempty?_eq h := LawfulBackwardPattern.dropSuffixOfNonempty?_eq (pat := (· == c)) h + skipSuffixOfNonempty?_eq h := LawfulBackwardPattern.skipSuffixOfNonempty?_eq (pat := (· == c)) h endsWith_eq s := LawfulBackwardPattern.endsWith_eq (pat := (· == c)) s instance {c : Char} : ToBackwardSearcher c (ToBackwardSearcher.DefaultBackwardSearcher c) := diff --git a/src/Init/Data/String/Pattern/Pred.lean b/src/Init/Data/String/Pattern/Pred.lean index f16d1764b8..7438699ce6 100644 --- a/src/Init/Data/String/Pattern/Pred.lean +++ b/src/Init/Data/String/Pattern/Pred.lean @@ -88,12 +88,12 @@ end Decidable @[default_instance] instance {p : Char → Bool} : BackwardPattern p where - dropSuffixOfNonempty? s h := + skipSuffixOfNonempty? 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 := + skipSuffix? s := if h : s.endPos = s.startPos then none else if p ((s.endPos.prev h).get (by simp)) then @@ -108,17 +108,17 @@ instance {p : Char → Bool} : BackwardPattern p where instance {p : Char → Bool} : StrictBackwardPattern p where ne_endPos {s h q} := by - simp only [BackwardPattern.dropSuffixOfNonempty?, Option.ite_none_right_eq_some, + simp only [BackwardPattern.skipSuffixOfNonempty?, 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?, + skipSuffixOfNonempty?_eq {s h} := by + simp [BackwardPattern.skipSuffixOfNonempty?, BackwardPattern.skipSuffix?, Eq.comm (a := s.endPos), Slice.startPos_eq_endPos_iff, h] endsWith_eq {s} := by - simp only [BackwardPattern.endsWith, BackwardPattern.dropSuffix?] + simp only [BackwardPattern.endsWith, BackwardPattern.skipSuffix?] split <;> (try split) <;> simp_all @[default_instance] @@ -128,15 +128,15 @@ instance {p : Char → Bool} : ToBackwardSearcher p (ToBackwardSearcher.DefaultB namespace Decidable 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 + skipSuffixOfNonempty? s h := BackwardPattern.skipSuffixOfNonempty? (decide <| p ·) s h + skipSuffix? s := BackwardPattern.skipSuffix? (decide <| p ·) s endsWith s := BackwardPattern.endsWith (decide <| p ·) s instance {p : Char → Prop} [DecidablePred p] : StrictBackwardPattern p where ne_endPos h q := StrictBackwardPattern.ne_endPos (pat := (decide <| p ·)) h q instance {p : Char → Prop} [DecidablePred p] : LawfulBackwardPattern p where - dropSuffixOfNonempty?_eq h := LawfulBackwardPattern.dropSuffixOfNonempty?_eq (pat := (decide <| p ·)) h + skipSuffixOfNonempty?_eq h := LawfulBackwardPattern.skipSuffixOfNonempty?_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) := diff --git a/src/Init/Data/String/Pattern/String.lean b/src/Init/Data/String/Pattern/String.lean index 942472d8af..49e2541d21 100644 --- a/src/Init/Data/String/Pattern/String.lean +++ b/src/Init/Data/String/Pattern/String.lean @@ -316,7 +316,7 @@ def endsWith (pat : Slice) (s : Slice) : Bool := false @[inline] -def dropSuffix? (pat : Slice) (s : Slice) : Option s.Pos := +def skipSuffix? (pat : Slice) (s : Slice) : Option s.Pos := if endsWith pat s then some <| s.pos! <| s.endPos.offset.unoffsetBy pat.rawEndPos else @@ -324,11 +324,11 @@ def dropSuffix? (pat : Slice) (s : Slice) : Option s.Pos := instance {pat : Slice} : BackwardPattern pat where endsWith := endsWith pat - dropSuffix? := dropSuffix? pat + skipSuffix? := skipSuffix? pat instance {pat : String} : BackwardPattern pat where endsWith := endsWith pat.toSlice - dropSuffix? := dropSuffix? pat.toSlice + skipSuffix? := skipSuffix? pat.toSlice end BackwardSliceSearcher diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean index aa2c5d4855..f037bc12c5 100644 --- a/src/Init/Data/String/Slice.lean +++ b/src/Init/Data/String/Slice.lean @@ -328,6 +328,26 @@ def splitInclusive (s : Slice) (pat : ρ) [ToForwardSearcher pat σ] : Std.Iter (α := SplitInclusiveIterator pat s) Slice := { internalState := .operating s.startPos (ToForwardSearcher.toSearcher pat s) } +/-- +If {name}`pat` matches a prefix of {name}`s`, returns the position at the start of the remainder. +Returns {name}`none` otherwise. + +This function is generic over all currently supported patterns. +-/ +@[inline] +def skipPrefix? (s : Slice) (pat : ρ) [ForwardPattern pat] : Option s.Pos := + ForwardPattern.skipPrefix? pat s + +/-- +If {name}`pat` matches a prefix at {name}`pos`, returns the position after the end of the match. +Returns {name}`none` otherwise. + +This function is generic over all currently supported patterns. +-/ +@[inline] +def Pos.skip? {s : Slice} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos := + ((s.sliceFrom pos).skipPrefix? pat).map Pos.ofSliceFrom + /-- If {name}`pat` matches a prefix of {name}`s`, returns the remainder. Returns {name}`none` otherwise. @@ -344,7 +364,7 @@ Examples: -/ @[inline] def dropPrefix? (s : Slice) (pat : ρ) [ForwardPattern pat] : Option Slice := - (ForwardPattern.skipPrefix? pat s).map s.sliceFrom + (s.skipPrefix? pat).map s.sliceFrom /-- If {name}`pat` matches a prefix of {name}`s`, returns the remainder. Returns {name}`s` unmodified @@ -400,6 +420,28 @@ Examples: def drop (s : Slice) (n : Nat) : Slice := s.sliceFrom (s.startPos.nextn n) +/-- +Advances {name}`pos` as long as {name}`pat` matches. +-/ +@[specialize pat] +def Pos.skipWhile {s : Slice} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : s.Pos := + if let some nextCurr := ForwardPattern.skipPrefix? pat (s.sliceFrom pos) then + if pos < Pos.ofSliceFrom nextCurr then + skipWhile (Pos.ofSliceFrom nextCurr) pat + else + pos + else + pos +termination_by pos + +/-- +Returns the position after the longest prefix of {name}`s` for which {name}`pat` matches +(potentially repeatedly). +-/ +@[inline] +def skipPrefixWhile (s : Slice) (pat : ρ) [ForwardPattern pat] : s.Pos := + s.startPos.skipWhile pat + /-- Creates a new slice that contains the longest prefix of {name}`s` for which {name}`pat` matched (potentially repeatedly). @@ -412,18 +454,7 @@ Examples: -/ @[inline] def dropWhile (s : Slice) (pat : ρ) [ForwardPattern pat] : Slice := - go s.startPos -where - @[specialize pat] - go (curr : s.Pos) : Slice := - if let some nextCurr := ForwardPattern.skipPrefix? pat (s.sliceFrom curr) then - if curr < Pos.ofSliceFrom nextCurr then - go (Pos.ofSliceFrom nextCurr) - else - s.sliceFrom curr - else - s.sliceFrom curr - termination_by curr + s.sliceFrom (s.skipPrefixWhile pat) /-- Removes leading whitespace from a slice by moving its start position to the first non-whitespace @@ -472,18 +503,7 @@ Examples: -/ @[inline] def takeWhile (s : Slice) (pat : ρ) [ForwardPattern pat] : Slice := - go s.startPos -where - @[specialize pat] - go (curr : s.Pos) : Slice := - if let some nextCurr := ForwardPattern.skipPrefix? pat (s.sliceFrom curr) then - if curr < Pos.ofSliceFrom nextCurr then - go (Pos.ofSliceFrom nextCurr) - else - s.sliceTo curr - else - s.sliceTo curr - termination_by curr + s.sliceTo (s.skipPrefixWhile pat) /-- Finds the position of the first match of the pattern {name}`pat` in a slice {name}`s`. If there @@ -668,6 +688,26 @@ def revSplit (s : Slice) (pat : ρ) [ToBackwardSearcher pat σ] : Std.Iter (α := RevSplitIterator pat s) Slice := { internalState := .operating s.endPos (ToBackwardSearcher.toSearcher pat s) } +/-- +If {name}`pat` matches a suffix of {name}`s`, returns the position at the beginning of the suffix. +Returns {name}`none` otherwise. + +This function is generic over all currently supported patterns. +-/ +@[inline] +def skipSuffix? (s : Slice) (pat : ρ) [BackwardPattern pat] : Option s.Pos := + BackwardPattern.skipSuffix? pat s + +/-- +If {name}`pat` matches a suffix at {name}`pos`, returns the position at the beginning of the match. +Returns {name}`none` otherwise. + +This function is generic over all currently supported patterns. +-/ +@[inline] +def Pos.revSkip? {s : Slice} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos := + ((s.sliceFrom pos).skipPrefix? pat).map Pos.ofSliceFrom + /-- If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise. @@ -684,7 +724,7 @@ Examples: -/ @[inline] def dropSuffix? (s : Slice) (pat : ρ) [BackwardPattern pat] : Option Slice := - (BackwardPattern.dropSuffix? pat s).map s.sliceTo + (s.skipSuffix? pat).map s.sliceTo /-- If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`s` unmodified @@ -719,6 +759,28 @@ Examples: def dropEnd (s : Slice) (n : Nat) : Slice := s.sliceTo (s.endPos.prevn n) +/-- +Rewinds {name}`pos` as long as {name}`pat` matches. +-/ +@[specialize pat] +def Pos.revSkipWhile {s : Slice} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : s.Pos := + if let some nextCurr := BackwardPattern.skipSuffix? pat (s.sliceTo pos) then + if Pos.ofSliceTo nextCurr < pos then + revSkipWhile (Pos.ofSliceTo nextCurr) pat + else + pos + else + pos +termination_by pos.down + +/-- +Returns the position a the start of the longest suffix of {name}`s` for which {name}`pat` matches +(potentially repeatedly). +-/ +@[inline] +def skipSuffixWhile (s : Slice) (pat : ρ) [BackwardPattern pat] : s.Pos := + s.endPos.revSkipWhile pat + /-- Creates a new slice that contains the longest suffix of {name}`s` for which {name}`pat` matched (potentially repeatedly). @@ -730,18 +792,7 @@ Examples: -/ @[inline] def dropEndWhile (s : Slice) (pat : ρ) [BackwardPattern pat] : Slice := - go s.endPos -where - @[specialize pat] - go (curr : s.Pos) : Slice := - if let some nextCurr := BackwardPattern.dropSuffix? pat (s.sliceTo curr) then - if Pos.ofSliceTo nextCurr < curr then - go (Pos.ofSliceTo nextCurr) - else - s.sliceTo curr - else - s.sliceTo curr - termination_by curr.down + s.sliceTo (s.skipSuffixWhile pat) /-- Removes trailing whitespace from a slice by moving its end position to the last non-whitespace @@ -789,18 +840,7 @@ Examples: -/ @[inline] def takeEndWhile (s : Slice) (pat : ρ) [BackwardPattern pat] : Slice := - go s.endPos -where - @[specialize pat] - go (curr : s.Pos) : Slice := - if let some nextCurr := BackwardPattern.dropSuffix? pat (s.sliceTo curr) then - if Pos.ofSliceTo nextCurr < curr then - go (Pos.ofSliceTo nextCurr) - else - s.sliceFrom curr - else - s.sliceFrom curr - termination_by curr.down + s.sliceFrom (s.skipSuffixWhile pat) /-- Finds the position of the first match of the pattern {name}`pat` in a slice, starting diff --git a/src/Init/Data/String/TakeDrop.lean b/src/Init/Data/String/TakeDrop.lean index c2bb547bc0..2ead6dc33d 100644 --- a/src/Init/Data/String/TakeDrop.lean +++ b/src/Init/Data/String/TakeDrop.lean @@ -208,6 +208,39 @@ def dropRightWhile (s : String) (p : Char → Bool) : String := def Slice.dropRightWhile (s : Slice) (p : Char → Bool) : Slice := s.dropEndWhile p +/-- +If {name}`pat` matches a prefix of {name}`s`, returns the position at the start of the remainder. +Returns {name}`none` otherwise. + +This function is generic over all currently supported patterns. +-/ +@[inline] def skipPrefix? (s : String) (pat : ρ) [ForwardPattern pat] : Option s.Pos := + (s.toSlice.skipPrefix? pat).map Pos.ofToSlice + +/-- +Returns the position after the longest prefix of {name}`s` for which {name}`pat` matches +(potentially repeatedly). +-/ +@[inline] def skipPrefixWhile (s : String) (pat : ρ) [ForwardPattern pat] : s.Pos := + Pos.ofToSlice (s.toSlice.skipPrefixWhile pat) + +/-- +If {name}`pat` matches at {name}`pos`, returns the position after the end of the match. +Returns {name}`none` otherwise. + +This function is generic over all currently supported patterns. +-/ +@[inline] +def Pos.skip? {s : String} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos := + (pos.toSlice.skip? pat).map Pos.ofToSlice + +/-- +Advances {name}`pos` as long as {name}`pat` matches. +-/ +@[inline] +def Pos.skipWhile {s : String} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : s.Pos := + Pos.ofToSlice (pos.toSlice.skipWhile pat) + /-- Checks whether the first string ({name}`s`) begins with the pattern ({name}`pat`). @@ -258,6 +291,39 @@ Examples: @[inline] def endsWith (s : String) (pat : ρ) [BackwardPattern pat] : Bool := s.toSlice.endsWith pat +/-- +If {name}`pat` matches a suffix of {name}`s`, returns the position at the beginning of the suffix. +Returns {name}`none` otherwise. + +This function is generic over all currently supported patterns. +-/ +@[inline] def skipSuffix? (s : String) (pat : ρ) [BackwardPattern pat] : Option s.Pos := + (s.toSlice.skipSuffix? pat).map Pos.ofToSlice + +/-- +Returns the position at the start of the longest suffix of {name}`s` for which {name}`pat` matches +(potentially repeatedly). +-/ +@[inline] def skipSuffixWhile (s : String) (pat : ρ) [BackwardPattern pat] : s.Pos := + Pos.ofToSlice (s.toSlice.skipSuffixWhile pat) + +/-- +If {name}`pat` matches at {name}`pos`, returns the position after the end of the match. +Returns {name}`none` otherwise. + +This function is generic over all currently supported patterns. +-/ +@[inline] +def Pos.revSkip? {s : String} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos := + (pos.toSlice.revSkip? pat).map Pos.ofToSlice + +/-- +Rewinds {name}`pos` as long as {name}`pat` matches. +-/ +@[inline] +def Pos.revSkipWhile {s : String} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : s.Pos := + Pos.ofToSlice (pos.toSlice.revSkipWhile pat) + /-- Removes trailing whitespace from a string by returning a slice whose end position is the last non-whitespace character, or the start position if there is no non-whitespace character.