structure String.Slice.Pattern.Model.SlicesFrom {s : Slice} (startPos : s.Pos) : Type

Represents a list of subslices of a slice s, the first of which starts at the given position startPos. This is a natural type for a split routine to return.

• l : List s.Subslice
• any_head? : Option.any (fun (x : s.Subslice) => decide (x.startInclusive = startPos)) self.l.head? = true

theorem String.Slice.Pattern.Model.SlicesFrom.ext {s : Slice} {startPos : s.Pos} {x y : SlicesFrom startPos} (l : x.l = y.l) : x = y

theorem String.Slice.Pattern.Model.SlicesFrom.ext_iff {s : Slice} {startPos : s.Pos} {x y : SlicesFrom startPos} : x = y ↔ x.l = y.l

def String.Slice.Pattern.Model.SlicesFrom.at {s : Slice} (pos : s.Pos) : SlicesFrom pos

A SlicesFrom consisting of a single empty subslice at the position pos.

Equations

• String.Slice.Pattern.Model.SlicesFrom.at pos = { l := [s.subslice pos pos ⋯], any_head? := ⋯ }

@[simp]

theorem String.Slice.Pattern.Model.SlicesFrom.l_at {s : Slice} (pos : s.Pos) : («at» pos).l = [s.subslice pos pos ⋯]

def String.Slice.Pattern.Model.SlicesFrom.append {s : Slice} {p₁ p₂ : s.Pos} (l₁ : SlicesFrom p₁) (l₂ : SlicesFrom p₂) : SlicesFrom p₁

Concatenating two SlicesFrom yields a SlicesFrom from the first position.

Equations

• l₁.append l₂ = { l := l₁.l ++ l₂.l, any_head? := ⋯ }

@[simp]

theorem String.Slice.Pattern.Model.SlicesFrom.l_append {s : Slice} {p₁ p₂ : s.Pos} {l₁ : SlicesFrom p₁} {l₂ : SlicesFrom p₂} : (l₁.append l₂).l = l₁.l ++ l₂.l

def String.Slice.Pattern.Model.SlicesFrom.extend {s : Slice} (p₁ : s.Pos) {p₂ : s.Pos} (h : p₁ ≤ p₂) (l : SlicesFrom p₂) : SlicesFrom p₁

Given a SlicesFrom p₂ and a position p₁ such that p₁ ≤ p₂, obtain a SlicesFrom p₁ by extending the left end of the first subslice to from p₂ to p₁.

Equations

• String.Slice.Pattern.Model.SlicesFrom.extend p₁ h l = { l := match l.l, ⋯ with | st :: sts, h_1 => st.extendLeft p₁ ⋯ :: sts, any_head? := ⋯ }

@[simp]

theorem String.Slice.Pattern.Model.SlicesFrom.l_extend {s : Slice} {p₁ p₂ : s.Pos} (h : p₁ ≤ p₂) {l : SlicesFrom p₂} : (extend p₁ h l).l = match l.l, ⋯ with | st :: sts, h_1 => st.extendLeft p₁ ⋯ :: sts

@[simp]

theorem String.Slice.Pattern.Model.SlicesFrom.extend_self {s : Slice} {p₁ : s.Pos} (l : SlicesFrom p₁) : extend p₁ ⋯ l = l

@[simp]

theorem String.Slice.Pattern.Model.SlicesFrom.extend_extend {s : Slice} {p₀ p₁ p₂ : s.Pos} {h : p₀ ≤ p₁} {h' : p₁ ≤ p₂} {l : SlicesFrom p₂} : extend p₀ h (extend p₁ h' l) = extend p₀ ⋯ l

@[irreducible]

noncomputable def String.Slice.Pattern.Model.split {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {s : Slice} (start : s.Pos) : SlicesFrom start

Noncomputable model implementation of String.Slice.splitToSubslice based on ForwardPatternModel. This is supposed to be simple enough to allow deriving higher-level API lemmas about the public splitting functions.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem String.Slice.Pattern.Model.split_endPos {ρ : Type} {pat : ρ} [ForwardPatternModel pat] {s : Slice} : Model.split pat s.endPos = SlicesFrom.at s.endPos

theorem String.Slice.Pattern.Model.split_eq_of_isLongestMatchAt {ρ : Type} {pat : ρ} [ForwardPatternModel pat] {s : Slice} {start stop : s.Pos} (h : IsLongestMatchAt pat start stop) : Model.split pat start = (SlicesFrom.at start).append (Model.split pat stop)

theorem String.Slice.Pattern.Model.split_eq_of_not_matchesAt {ρ : Type} {pat : ρ} [ForwardPatternModel pat] {s : Slice} {start stop : s.Pos} (h₀ : start ≤ stop) (h : ∀ (p : s.Pos), start ≤ p → p < stop → ¬MatchesAt pat p) : Model.split pat start = SlicesFrom.extend start h₀ (Model.split pat stop)

theorem String.Slice.Pattern.toList_splitToSubslice_eq_modelSplit {ρ : Type} (pat : ρ) [Model.ForwardPatternModel pat] {σ : Slice → Type} [ToForwardSearcher pat σ] [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] (s : Slice) : (s.splitToSubslice pat).toList = (Model.split pat s.startPos).l