DTAIE7PK6TZLNSBQGENS6RT7FFOTMAPSE6ZTPDADINGJF5NTHLWQC /-- Helper lemma for termination proofs -/private theorem sizeOf_get_lt_internal (cs : Array PieceTree) (s : Stats) (i : Nat) (h : i < cs.size) :sizeOf (cs[i]) < sizeOf (internal cs s) := bycases cs with | mk data =>-- 1. Relate Array access to List accesshave eq : (Array.mk data)[i] = data.get ⟨i, h⟩ := rflrw [eq]-- 2. Use standard List size propertyhave lt_list : sizeOf (data.get ⟨i, h⟩) < sizeOf data :=List.sizeOf_lt_of_mem (List.get_mem data ⟨i, h⟩)-- 3. Prove data < internal cs s using simplificationhave lt_internal : sizeOf data < sizeOf (internal (Array.mk data) s) := bygrind only [internal.sizeOf_spec, Array.mk.sizeOf_spec]-- 4. Transitivityapply Nat.lt_trans lt_list lt_internal
let lastIdx := cs1.size - 1let lastChild := cs1[lastIdx]!let newLast := concat lastChild r
if h_empty : cs1.size = 0 then relselet lastIdx := cs1.size - 1have h_bound : lastIdx < cs1.size := Nat.pred_lt h_emptylet lastChild := cs1[lastIdx]let newLast := concat lastChild r
if newLast.height == lastChild.height thenmkInternal (cs1.set! lastIdx newLast)elsematch newLast with| internal subChildren _ =>let newCs := cs1.pop ++ subChildrenif newCs.size <= NodeCapacity then mkInternal newCselselet mid := newCs.size / 2mkInternal #[mkInternal (newCs.extract 0 mid), mkInternal (newCs.extract mid newCs.size)]| _ => mkInternal (cs1.push newLast)
if newLast.height == lastChild.height thenmkInternal (cs1.set! lastIdx newLast)elsematch newLast with| internal subChildren _ =>let newCs := cs1.pop ++ subChildrenif newCs.size <= NodeCapacity then mkInternal newCselselet mid := newCs.size / 2mkInternal #[mkInternal (newCs.extract 0 mid), mkInternal (newCs.extract mid newCs.size)]| _ => mkInternal (cs1.push newLast)
match newFirst with| internal subChildren _ =>let newCs := subChildren ++ cs2.extract 1 cs2.sizeif newCs.size <= NodeCapacity then mkInternal newCselselet mid := newCs.size / 2mkInternal #[mkInternal (newCs.extract 0 mid), mkInternal (newCs.extract mid newCs.size)]| _ => mkInternal ((#[newFirst] ++ cs2))
have h_bound : 0 < cs2.size := Nat.pos_of_ne_zero h_emptylet firstChild := cs2[0]let newFirst := concat l firstChild
| leaf _ _, internal _ _ =>let firstChild := match r with | internal cs _ => cs[0]! | _ => emptylet newFirst := concat l firstChildmatch r with| internal cs2 _ =>if newFirst.height == firstChild.height thenmkInternal (cs2.set! 0 newFirst)elsematch newFirst with| internal subChildren _ =>let newCs := subChildren ++ cs2.extract 1 cs2.sizeif newCs.size <= NodeCapacity then mkInternal newCselselet mid := newCs.size / 2mkInternal #[mkInternal (newCs.extract 0 mid), mkInternal (newCs.extract mid newCs.size)]| _ => mkInternal ((#[newFirst] ++ cs2))| _ => empty
if newFirst.height == firstChild.height thenmkInternal (cs2.set! 0 newFirst)elsematch newFirst with| internal subChildren _ =>let newCs := subChildren ++ cs2.extract 1 cs2.sizeif newCs.size <= NodeCapacity then mkInternal newCselselet mid := newCs.size / 2mkInternal #[mkInternal (newCs.extract 0 mid), mkInternal (newCs.extract mid newCs.size)]| _ => mkInternal ((#[newFirst] ++ cs2))
| internal _ _, leaf _ _ =>let cs1 := match l with | internal cs _ => cs | _ => #[]let lastIdx := cs1.size - 1let lastChild := cs1[lastIdx]!let newLast := concat lastChild r
| (leaf ps1 s1, internal cs2 s2) =>if h_empty : cs2.size = 0 then lelsehave h_bound : 0 < cs2.size := Nat.pos_of_ne_zero h_emptylet firstChild := cs2[0]let newFirst := concat l firstChildif newFirst.height == firstChild.height thenmkInternal (cs2.set! 0 newFirst)elsematch newFirst with| internal subChildren _ =>let newCs := subChildren ++ cs2.extract 1 cs2.sizeif newCs.size <= NodeCapacity then mkInternal newCselselet mid := newCs.size / 2mkInternal #[mkInternal (newCs.extract 0 mid), mkInternal (newCs.extract mid newCs.size)]| _ => mkInternal ((#[newFirst] ++ cs2))
match newLast with| internal subChildren _ =>let newCs := cs1.pop ++ subChildrenif newCs.size <= NodeCapacity then mkInternal newCselselet mid := newCs.size / 2mkInternal #[mkInternal (newCs.extract 0 mid), mkInternal (newCs.extract mid newCs.size)]| _ => mkInternal (cs1.push newLast)
let lastIdx := cs1.size - 1have h_bound : lastIdx < cs1.size := Nat.pred_lt h_emptylet lastChild := cs1[lastIdx]let newLast := concat lastChild rif newLast.height == lastChild.height thenmkInternal (cs1.set! lastIdx newLast)elsematch newLast with| internal subChildren _ =>let newCs := cs1.pop ++ subChildrenif newCs.size <= NodeCapacity then mkInternal newCselselet mid := newCs.size / 2mkInternal #[mkInternal (newCs.extract 0 mid), mkInternal (newCs.extract mid newCs.size)]| _ => mkInternal (cs1.push newLast)termination_by sizeOf l + sizeOf rdecreasing_bysimp_wf-- Case 1: l.height > r.height· have hl : l = internal cs1 s1 := congrArg Prod.fst hrw [hl]try apply Nat.add_lt_add_rightapply sizeOf_get_lt_internal _ _ _ (by assumption)-- Case 2: l.height < r.height· have hr : r = internal cs2 s2 := congrArg Prod.snd hrw [hr]try apply Nat.add_lt_add_leftapply sizeOf_get_lt_internal _ _ _ (by assumption)-- Case 3: l is leaf, r is internal· have hr : r = internal cs2 s2 := congrArg Prod.snd hrw [hr]try apply Nat.add_lt_add_leftapply sizeOf_get_lt_internal _ _ _ (by assumption)-- Case 4: l is internal, r is leaf· have hl : l = internal cs1 s1 := congrArg Prod.fst hrw [hl]try apply Nat.add_lt_add_rightapply sizeOf_get_lt_internal _ _ _ (by assumption)
/-- Split the tree at a given character offset. -/partial def split (t : PieceTree) (offset : Nat) (pt : PieceTable) : (PieceTree × PieceTree) :=match t with| empty => (empty, empty)| leaf pieces s => splitLeaf pieces s pt offset| internal children curStats =>if offset == 0 then (empty, t)else if offset >= curStats.bytes then (t, empty)elselet rec scan (i : Nat) (accOff : Nat) : (PieceTree × PieceTree) :=if i >= children.size then (t, empty)elselet c := children[i]!if accOff + c.length > offset thenlet (cLeft, cRight) := split c (offset - accOff) pt
mutual/-- Split the tree at a given character offset. -/def split (t : PieceTree) (offset : Nat) (pt : PieceTable) : (PieceTree × PieceTree) :=match t with| empty => (empty, empty)| leaf pieces s => splitLeaf pieces s pt offset| internal children curStats =>if offset == 0 then (empty, t)else if offset >= curStats.bytes then (t, empty)elsesplitAux children offset pt 0 0termination_by (sizeOf t, 0)decreasing_bysimp_wf-- split -> splitAuxapply Prod.Lex.leftsimp +arith/-- Aux helper for internal node split to scan children -/def splitAux (children : Array PieceTree) (offset : Nat) (pt : PieceTable) (i : Nat) (accOff : Nat) : (PieceTree × PieceTree) :=if h : i < children.size thenlet c := children[i]if accOff + c.length > offset thenlet (cLeft, cRight) := split c (offset - accOff) ptlet leftChildren := (children.extract 0 i).push cLeftlet rightChildren := (#[cRight]).append (children.extract (i + 1) children.size)
let leftChildren := (children.extract 0 i).push cLeftlet rightChildren := (#[cRight]).append (children.extract (i + 1) children.size)
let leftFiltered := leftChildren.filter (fun c => c.length > 0)let rightFiltered := rightChildren.filter (fun c => c.length > 0)
let leftFiltered := leftChildren.filter (fun c => c.length > 0)let rightFiltered := rightChildren.filter (fun c => c.length > 0)
(mkInternal leftFiltered, mkInternal rightFiltered)elsesplitAux children offset pt (i + 1) (accOff + c.length)else(mkInternal children, empty)termination_by (sizeOf children, children.size - i)decreasing_byall_goals simp_wf-- splitAux -> split (c)· apply Prod.Lex.leftcases children with | mk data =>have lt_list : sizeOf (data.get ⟨i, h⟩) < sizeOf data :=List.sizeOf_lt_of_mem (List.get_mem data ⟨i, h⟩)have lt_array : sizeOf data < sizeOf (Array.mk data) := bygrind only [Array.mk.sizeOf_spec]exact Nat.lt_trans lt_list lt_array
/-- Find offset of the N-th newline (0-indexed). -/partial def findNthNewline (t : PieceTree) (n : Nat) (pt : PieceTable) : Nat :=match t with| empty => 0| leaf pieces _ =>let rec scanPieces (i : Nat) (remainingN : Nat) (accOffset : Nat) : Nat :=if i >= pieces.size then accOffsetelselet p := pieces[i]!if remainingN < p.lineBreaks thenlet buf := PieceTableHelper.getBuffer pt p.sourcelet rec scan (j : Nat) (cnt : Nat) : Nat :=if j >= p.length then jelseif buf[p.start + j]! == 10 thenif cnt == remainingN then jelse scan (j + 1) (cnt + 1)else scan (j + 1) cntaccOffset + (scan 0 0)
/-- Helper to scan pieces in a leaf for Nth newline -/def findNthNewlineLeaf (pieces : Array Piece) (n : Nat) (pt : PieceTable) (i : Nat) (accOffset : Nat) : Nat :=if h : i < pieces.size thenlet p := pieces[i]if n < p.lineBreaks thenlet buf := PieceTableHelper.getBuffer pt p.sourcelet rec scan (j : Nat) (cnt : Nat) : Nat :=if j >= p.length then j
scanPieces (i + 1) (remainingN - p.lineBreaks) (accOffset + p.length)scanPieces 0 n 0
if buf[p.start + j]! == 10 thenif cnt == n then jelse scan (j + 1) (cnt + 1)else scan (j + 1) cntaccOffset + (scan 0 0)elsefindNthNewlineLeaf pieces (n - p.lineBreaks) pt (i + 1) (accOffset + p.length)elseaccOffsettermination_by pieces.size - i
| internal children _ =>let rec scanChildren (i : Nat) (remainingN : Nat) (accOffset : Nat) : Nat :=if i >= children.size then accOffset
mutual/-- Find offset of the N-th newline (0-indexed). -/def findNthNewline (t : PieceTree) (n : Nat) (pt : PieceTable) : Nat :=match t with| empty => 0| leaf pieces _ => findNthNewlineLeaf pieces n pt 0 0| internal children _ => findNthNewlineAux children n pt 0 0termination_by (sizeOf t, 0)decreasing_bysimp_wf-- findNthNewline -> findNthNewlineAuxapply Prod.Lex.leftsimp +arithdef findNthNewlineAux (children : Array PieceTree) (n : Nat) (pt : PieceTable) (i : Nat) (accOffset : Nat) : Nat :=if h : i < children.size thenlet child := children[i]let childLines := child.lineBreaksif n < childLines thenaccOffset + findNthNewline child n pt
let child := children[i]!let childLines := child.lineBreaksif remainingN < childLines thenaccOffset + findNthNewline child remainingN ptelsescanChildren (i + 1) (remainingN - childLines) (accOffset + child.length)scanChildren 0 n 0
findNthNewlineAux children (n - childLines) pt (i + 1) (accOffset + child.length)elseaccOffsettermination_by (sizeOf children, children.size - i)decreasing_byall_goals simp_wf-- findNthNewlineAux -> findNthNewline· apply Prod.Lex.leftcases children with | mk data =>have eq : (Array.mk data)[i] = data.get ⟨i, h⟩ := rflrw [eq]have lt_list : sizeOf (data.get ⟨i, h⟩) < sizeOf data :=List.sizeOf_lt_of_mem (List.get_mem data ⟨i, h⟩)have lt_array : sizeOf data < sizeOf (Array.mk data) := bygrind only [Array.mk.sizeOf_spec]exact Nat.lt_trans lt_list lt_array-- findNthNewlineAux -> findNthNewlineAux· apply Prod.Lex.rightapply Nat.sub_lt_sub_left· exact h· exact Nat.lt_succ_self _end