GUD2J453E3UTRJZIEEUUJ3ZIGL72ETUXTO57XQIZ2Y3ZU3C2R55QC U45XPF3YKPXXRJ4MN24T2RV7GOL4FZKQSWX5P5I7WT4HC5XF4FHAC R6L2TITEEB2XRNCTCGETAQ6UBYRMDKYL6TCPA3KVQTBCMPSN5ZJQC 5SFTBD4FW6GQPKRUJBAII5R2EZPDYG6CH57BIJD4IVZBE6JZB2ZQC 6W6OJAUT3KLOXXKYR4GA3MG4ACLO2T4KX3SGD2KZDX6MYEZYTPHAC WRBKZMYVNHRWT7TTUGTDJ3TMWZB32QYW5PCLKTTVAJ2YF6OI3LTAC DTAIE7PK6TZLNSBQGENS6RT7FFOTMAPSE6ZTPDADINGJF5NTHLWQC #!/bin/bash# ConfigurationITERATIONS=${1:-10000}OUTPUT_DIR=".lake/build/bin"BENCH_EXE="$OUTPUT_DIR/bench"PERF_DATA="perf.data"echo "=== ViE Performance Profile Script ==="# 1. Build the benchmark executableecho "Building benchmark..."lake build benchif [ $? -ne 0 ]; thenecho "Error: Build failed."exit 1fiif [ ! -f "$BENCH_EXE" ]; thenecho "Error: Benchmark executable not found at $BENCH_EXE"exit 1fi# 2. Check for perfif ! command -v perf &> /dev/null; thenecho "Error: 'perf' command not found. Please install perf"exit 1fi# 3. Run perf recordecho "Running perf record with $ITERATIONS iterations..."echo "This may require sudo permissions for kernel-level profiling."perf record -g --call-graph dwarf "$BENCH_EXE" "$ITERATIONS"if [ $? -eq 0 ]; thenecho "=== Profile Complete ==="echo "To view the results, run:"echo " perf report"echo ""echo "To generate a flamegraph (if tools are installed):"echo " perf script | stackcollapse-perf.pl | flamegraph.pl > flamegraph.svg"elseecho "Error: perf record failed. You might need to run: sudo sysctl -w kernel.perf_event_paranoid=-1"fi
[[lean_exe]]name = "bench"root = "Test.Benchmark"[[lean_exe]]name = "tree-stats"root = "Test.TreeStats"
{ original := bytes, add := ByteArray.empty, tree := PieceTree.empty, undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }
{ original := bytes, addBuffers := #[], tree := PieceTree.empty, undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }
let len := min PieceTable.ChunkSize (totalSize - start)let lines := ViE.Unicode.countNewlines bytes start lenlet chars := ViE.Unicode.countChars bytes start lenlet piece := { source := .original, start := start, length := len, lineBreaks := lines, charCount := chars }
let len := min ChunkSize (totalSize - start)let lines := Unicode.countNewlines bytes start lenlet chars := Unicode.countChars bytes start lenlet piece : Piece := { source := BufferSource.original, start := start, length := len, lineBreaks := lines, charCount := chars }
{ original := bytes, add := ByteArray.empty, tree := tree, undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }
{ original := bytes, addBuffers := #[], tree := tree, undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }
| some (lastOff, lastAddOff) =>if offset == lastOff && lastAddOff == pt.add.size then
| some last =>let lastBuf := pt.addBuffers.getD last.bufferIdx ByteArray.emptylet isContig := offset == last.docOffsetlet isLastBuf := last.bufferIdx == pt.addBuffers.size - 1let isEndOfBuf := last.bufferOffset == lastBuf.sizeif isContig && isLastBuf && isEndOfBuf then
let params := if stack.length > pt.undoLimit then stack.take pt.undoLimit else stack(params, some (offset + text.utf8ByteSize, pt.add.size + text.utf8ByteSize))
let newCount := pt.undoStackCount + 1let (finalStack, finalCount) := if newCount > pt.undoLimit then (stack.take pt.undoLimit, pt.undoLimit) else (stack, newCount)(finalStack, finalCount, some { docOffset := offset + text.toUTF8.size, bufferIdx := pt.addBuffers.size, bufferOffset := text.toUTF8.size })
let params := if stack.length > pt.undoLimit then stack.take pt.undoLimit else stack(params, some (offset + text.utf8ByteSize, pt.add.size + text.utf8ByteSize))
let newCount := pt.undoStackCount + 1let (finalStack, finalCount) := if newCount > pt.undoLimit then (stack.take pt.undoLimit, pt.undoLimit) else (stack, newCount)(finalStack, finalCount, some { docOffset := offset + text.toUTF8.size, bufferIdx := pt.addBuffers.size, bufferOffset := text.toUTF8.size })
/--Delete a range of text.params:- offset: The starting byte offset of the range to delete.- length: The number of bytes to delete.- cursorOffset: The cursor position *after* this deletion, stored in the undo stackto restore cursor position when undoing this operation.-/
/-- Delete a range of text. -/
def PieceTable.lineCount (pt : PieceTable) : Nat :=let breaks := PieceTree.lineBreaks pt.treeif breaks == 0 then 1-- If the file ends with a newline, Vim doesn't count it as a new empty line-- unless it's preceded by another newline (e.g., "a\n\n" is 2 lines).else if pt.endsWithNewline then breakselse breaks + 1
import ViE.Data.PieceTable.Piece/-- A node in the B+ Piece Tree -/| empty| leaf (pieces : Array Piece) (stats : Stats)| internal (children : Array PieceTree) (stats : Stats)deriving Repr, Inhabitedstructure PieceTable whereoriginal : ByteArrayadd : ByteArraytree : PieceTreederiving Inhabitedend ViEundoStack : List (PieceTree × Nat) := []redoStack : List (PieceTree × Nat) := []undoLimit : Nat := 100lastInsert : Option (Nat × Nat) := noneinductive PieceTree : Type _ wherenamespace ViE
/-- Append text to add buffer -/def appendText (pt : PieceTable) (text : String) : (PieceTable × Piece) :=
/-- Append text to add buffer, splitting into chunks if necessary -/def appendText (pt : ViE.PieceTable) (text : String) : (ViE.PieceTable × Array ViE.Piece) :=
let start := pt.add.sizelet len := bytes.sizelet newAdd := pt.add ++ byteslet newLines := ViE.Unicode.countNewlines bytes 0 lenlet newChars := ViE.Unicode.countChars bytes 0 lenlet piece := { source := .add, start := start, length := len, lineBreaks := newLines, charCount := newChars }({ pt with add := newAdd }, piece)
let totalSize := bytes.sizelet bufferIdx := pt.addBuffers.sizelet newAddBuffers := pt.addBuffers.push byteslet rec splitChunks (start : Nat) (acc : Array ViE.Piece) : Array ViE.Piece :=if start >= totalSize then accelselet len := min ViE.ChunkSize (totalSize - start)let lines := ViE.Unicode.countNewlines bytes start lenlet chars := ViE.Unicode.countChars bytes start lenlet piece : ViE.Piece := {source := ViE.BufferSource.add bufferIdx,start := start,length := len,lineBreaks := lines,charCount := chars}splitChunks (start + len) (acc.push piece)termination_by totalSize - startdecreasing_bysimp_wfrw [Nat.sub_add_eq]have h : start < totalSize := Nat.lt_of_not_le (by assumption)apply Nat.sub_lt_self· have h1 : 0 < totalSize - start := Nat.sub_pos_of_lt happly Nat.lt_min.mprconstructor. show 0 < ViE.ChunkSizeunfold ViE.ChunkSizeexact Nat.zero_lt_succ _· assumption· apply Nat.min_le_rightlet ps := splitChunks 0 #[]({ pt with addBuffers := newAddBuffers }, ps)
/-- Split a piece into two at a given relative offset. -/def splitPiece (pt : PieceTable) (p : Piece) (offset : Nat) : (Piece × Piece) :=
/-- Split a piece into two at a given relative offset -/def splitPiece (p : ViE.Piece) (offset : Nat) (pt : ViE.PieceTable) : (ViE.Piece × ViE.Piece) :=
let rightChars := p.charCount - leftCharslet leftP := { p with length := leftLen, lineBreaks := leftLines, charCount := leftChars }let rightP := { p with start := p.start + leftLen, length := rightLen, lineBreaks := rightLines, charCount := rightChars }(leftP, rightP)
let leftPiece : ViE.Piece := { p with length := leftLen, lineBreaks := leftLines, charCount := leftChars }let rightPiece : ViE.Piece := { p withstart := p.start + leftLen,length := rightLen,lineBreaks := p.lineBreaks - leftLines,charCount := p.charCount - leftChars}(leftPiece, rightPiece)
def stats : PieceTree → Stats| empty => Stats.empty| leaf _ s => s| internal _ s => sdef length (t : PieceTree) : Nat := t.stats.bytesdef lineBreaks (t : PieceTree) : Nat := t.stats.linesdef height (t : PieceTree) : Nat := t.stats.height/-- Helper to construct a leaf node from pieces -/def mkLeaf (pieces : Array Piece) : PieceTree :=let stats := pieces.foldl (fun s p =>{ s with bytes := s.bytes + p.length, lines := s.lines + p.lineBreaks, chars := s.chars + p.charCount }){ bytes := 0, lines := 0, chars := 0, height := 1 }leaf pieces stats
def stats (t : ViE.PieceTree) : ViE.Stats :=match t with| ViE.PieceTree.empty => ViE.Stats.empty| ViE.PieceTree.leaf _ s => s| ViE.PieceTree.internal _ s => s
/-- Helper to construct an internal node from children -/def mkInternal (children : Array PieceTree) : PieceTree :=if children.isEmpty then emptyelselet firstHeight := (children[0]!).heightlet h := firstHeight + 1let stats := children.foldl (fun s c =>let cs := c.stats{ s with bytes := s.bytes + cs.bytes, lines := s.lines + cs.lines, chars := s.chars + cs.chars }){ bytes := 0, lines := 0, chars := 0, height := h }internal children stats
def length (t : ViE.PieceTree) : Nat := (stats t).bytesdef lineBreaks (t : ViE.PieceTree) : Nat := (stats t).linesdef height (t : ViE.PieceTree) : Nat := (stats t).height
/-- 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
/-- Create a leaf node -/def mkLeaf (pieces : Array ViE.Piece) : ViE.PieceTree :=let s := pieces.foldl (fun acc p => acc + (ViE.Stats.ofPiece p)) ViE.Stats.emptyViE.PieceTree.leaf pieces s
/-- Concatenate two trees -/def concat (l : PieceTree) (r : PieceTree) : PieceTree :=match h : (l, r) with| (empty, _) => r| (_, empty) => l
/-- Create an internal node -/def mkInternal (children : Array ViE.PieceTree) : ViE.PieceTree :=let s := children.foldl (fun acc c => acc + (stats c)) ViE.Stats.emptylet s := { s with height := s.height + 1 }ViE.PieceTree.internal children s
| (leaf ps1 _, leaf ps2 _) =>let ps := ps1 ++ ps2if ps.size <= NodeCapacity thenmkLeaf pselse-- Split into two leaveslet mid := ps.size / 2let l := mkLeaf (ps.extract 0 mid)let r := mkLeaf (ps.extract mid ps.size)mkInternal #[l, r]
/-- Efficiently concatenate a list of pieces into a tree -/partial def fromPieces (pieces : Array ViE.Piece) : ViE.PieceTree :=if pieces.isEmpty then ViE.PieceTree.emptyelse if pieces.size <= ViE.NodeCapacity thenmkLeaf pieceselselet mid := pieces.size / 2let left := fromPieces (pieces.extract 0 mid)let right := fromPieces (pieces.extract mid pieces.size)mkInternal #[left, right]
| (internal cs1 s1, internal cs2 s2) =>if l.height == r.height thenlet cs := cs1 ++ cs2if cs.size <= NodeCapacity thenmkInternal cselselet mid := cs.size / 2let l := mkInternal (cs.extract 0 mid)let r := mkInternal (cs.extract mid cs.size)mkInternal #[l, r]else if l.height > r.height then-- Append r to the last child of lif 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
/-- Concatenate two trees while maintaining B+ tree invariants -/partial def concat (l : ViE.PieceTree) (r : ViE.PieceTree) : ViE.PieceTree :=match l, r with| ViE.PieceTree.empty, _ => r| _, ViE.PieceTree.empty => l
if newLast.height == lastChild.height thenmkInternal (cs1.set! lastIdx newLast)
| ViE.PieceTree.leaf ps1 _, ViE.PieceTree.leaf ps2 _ =>-- Try to merge the last piece of ps1 with the first piece of ps2if ps1.size > 0 && ps2.size > 0 thenlet p1 := ps1.back!let p2 := ps2[0]!if p1.source == p2.source && p1.start + p1.length == p2.start thenlet mergedPiece : ViE.Piece := { p1 withlength := p1.length + p2.length,lineBreaks := p1.lineBreaks + p2.lineBreaks,charCount := p1.charCount + p2.charCount}let ps := (ps1.pop).push mergedPiece ++ (ps2.extract 1 ps2.size)if ps.size <= ViE.NodeCapacity thenmkLeaf ps
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)else -- l.height < r.heightif h_empty : cs2.size = 0 then l
let mid := ps.size / 2mkInternal #[mkLeaf (ps.extract 0 mid), mkLeaf (ps.extract mid ps.size)]
have h_bound : 0 < cs2.size := Nat.pos_of_ne_zero h_emptylet firstChild := cs2[0]let newFirst := concat l firstChild
let ps := ps1 ++ ps2if ps.size <= ViE.NodeCapacity then mkLeaf pselse mkInternal #[mkLeaf ps1, mkLeaf ps2]else if ps1.size > 0 then lelse r
if newFirst.height == firstChild.height thenmkInternal (cs2.set! 0 newFirst)
| ViE.PieceTree.internal cs1 _, ViE.PieceTree.internal cs2 _ =>let h1 := height llet h2 := height rif h1 == h2 then-- Merge boundary childrenlet lastChild := cs1.back!let firstChild := cs2[0]!let merged := concat lastChild firstChildmatch merged with| ViE.PieceTree.internal newCS s =>if s.height == h1 then-- newCS is at the same level as siblingslet combined := (cs1.pop) ++ newCS ++ (cs2.extract 1 cs2.size)if combined.size <= ViE.NodeCapacity then mkInternal combinedelselet mid := combined.size / 2mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]
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))| (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)
-- height did not increase, just one childlet combined := (cs1.pop).push merged ++ (cs2.extract 1 cs2.size)if combined.size <= ViE.NodeCapacity then mkInternal combinedelselet mid := combined.size / 2mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]| _ =>let combined := (cs1.pop).push merged ++ (cs2.extract 1 cs2.size)if combined.size <= ViE.NodeCapacity then mkInternal combined
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))| (internal cs1 s1, leaf ps2 s2) =>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 rif newLast.height == lastChild.height thenmkInternal (cs1.set! lastIdx newLast)
let mid := combined.size / 2mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]else if h1 > h2 then-- Insert r into l's right sidelet lastChild := cs1.back!let newLast := concat lastChild rmatch newLast with| ViE.PieceTree.internal newChildren s =>if s.height == h1 then-- Split happened at l's levellet combined := (cs1.pop) ++ newChildrenif combined.size <= ViE.NodeCapacity then mkInternal combinedelselet mid := combined.size / 2mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]
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)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 a leaf node at a specific piece index and internal offset -/def splitLeaf (pieces : Array Piece) (stats : Stats) (pt : PieceTable) (offset : Nat) : (PieceTree × PieceTree) :=let rec findPiece (i : Nat) (currentOff : Nat) : (Nat × Nat) :=if i >= pieces.size then (pieces.size, currentOff)elselet p := pieces[i]!if currentOff + p.length > offset then (i, currentOff)else findPiece (i + 1) (currentOff + p.length)let (idx, pStart) := findPiece 0 0if idx >= pieces.size then(leaf pieces stats, empty)elselet p := pieces[idx]!let splitOff := offset - pStartif splitOff == 0 thenlet leftArr := pieces.extract 0 idxlet rightArr := pieces.extract idx pieces.size(mkLeaf leftArr, mkLeaf rightArr)else if splitOff == p.length thenlet leftArr := pieces.extract 0 (idx + 1)let rightArr := pieces.extract (idx + 1) pieces.size(mkLeaf leftArr, mkLeaf rightArr)
mkInternal ((cs1.pop).push newLast)| _ => mkInternal ((cs1.pop).push newLast)
let (p1, p2) := PieceTableHelper.splitPiece pt p splitOfflet leftPieces := (pieces.extract 0 idx).push p1let rightPieces := (#[p2]).append (pieces.extract (idx + 1) pieces.size)(mkLeaf leftPieces, mkLeaf rightPieces)
-- Insert l into r's left sidelet firstChild := cs2[0]!let newFirst := concat l firstChildmatch newFirst with| ViE.PieceTree.internal newChildren s =>if s.height == h2 thenlet combined := newChildren ++ (cs2.extract 1 cs2.size)if combined.size <= ViE.NodeCapacity then mkInternal combinedelselet mid := combined.size / 2mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]elsemkInternal (#[newFirst] ++ (cs2.extract 1 cs2.size))| _ => mkInternal (#[newFirst] ++ (cs2.extract 1 cs2.size))
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)
/-- Split the tree at a given byte offset -/partial def split (t : ViE.PieceTree) (offset : Nat) (pt : ViE.PieceTable) : (ViE.PieceTree × ViE.PieceTree) :=match t with| ViE.PieceTree.empty => (ViE.PieceTree.empty, ViE.PieceTree.empty)| ViE.PieceTree.leaf pieces _ =>let rec findSplitLeaf (i : Nat) (accOffset : Nat) : (ViE.PieceTree × ViE.PieceTree) :=if i >= pieces.size then (t, ViE.PieceTree.empty)
splitAux 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 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-- splitAux -> splitAux (i+1)· apply Prod.Lex.rightapply Nat.sub_lt_sub_left· exact h· exact Nat.lt_succ_self _end/-- Delete range [offset, offset + length) -/def delete (t : PieceTree) (offset : Nat) (length : Nat) (pt : PieceTable) : PieceTree :=if length == 0 then telselet (l, r) := split t offset ptlet (_, r') := split r length ptconcat l r'/-- 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
let p := pieces[i]!if offset < accOffset + p.length thenlet relOffset := offset - accOffsetif relOffset == 0 then(mkLeaf (pieces.extract 0 i), mkLeaf (pieces.extract i pieces.size))elselet (p1, p2) := PieceTableHelper.splitPiece p relOffset pt(mkLeaf ((pieces.extract 0 i).push p1), mkLeaf (#[p2] ++ (pieces.extract (i + 1) pieces.size)))
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 - imutual/-- 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 ptelsefindNthNewlineAux 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/-- Get substring of tree from start to end offset -/partial def getSubstring (t : PieceTree) (startOff endOff : Nat) (pt : PieceTable) : String :=if startOff >= endOff then ""elselet rec traverse (t : PieceTree) (currentOff : Nat) : String :=let tLen := t.lengthif currentOff + tLen <= startOff || currentOff >= endOff then ""elsematch t with| empty => ""| leaf pieces _ =>let rec scan (i : Nat) (off : Nat) (acc : String) : String :=if i >= pieces.size then accelselet p := pieces[i]!let pStart := offlet pEnd := off + p.lengthlet readStart := max startOff pStartlet readEnd := min endOff pEndif readStart < readEnd thenlet buf := PieceTableHelper.getBuffer pt p.sourcelet sliceStart := p.start + (readStart - pStart)let sliceEnd := p.start + (readEnd - pStart)let str := String.fromUTF8! (buf.extract sliceStart sliceEnd)scan (i + 1) pEnd (acc ++ str)elsescan (i + 1) pEnd accscan 0 currentOff ""| internal children _ =>let rec scanInternal (i : Nat) (off : Nat) (acc : String) : String :=if i >= children.size then accelselet c := children[i]!let s := traverse c offscanInternal (i + 1) (off + c.length) (acc ++ s)scanInternal 0 currentOff ""traverse t 0/-- Get total string length of a range (counting chars, not bytes, without allocation) -/partial def countCharsInRange (t : PieceTree) (startOff endOff : Nat) (pt : PieceTable) : Nat :=if startOff >= endOff then 0elselet rec traverse (t : PieceTree) (currentOff : Nat) : Nat :=let tLen := t.lengthif currentOff + tLen <= startOff || currentOff >= endOff then 0else if currentOff >= startOff && currentOff + tLen <= endOff thent.stats.chars
findSplitLeaf (i + 1) (accOffset + p.length)findSplitLeaf 0 0| ViE.PieceTree.internal children _ =>let rec findSplitInternal (i : Nat) (accOffset : Nat) : (ViE.PieceTree × ViE.PieceTree) :=if i >= children.size then (t, ViE.PieceTree.empty)
match t with| empty => 0| leaf pieces _ =>let rec scan (i : Nat) (off : Nat) (acc : Nat) : Nat :=if i >= pieces.size then accelselet p := pieces[i]!let pStart := offlet pEnd := off + p.lengthif pEnd <= startOff || pStart >= endOff thenscan (i + 1) pEnd accelse if pStart >= startOff && pEnd <= endOff thenscan (i + 1) pEnd (acc + p.charCount)elselet readStart := max startOff pStartlet readEnd := min endOff pEndlet buf := PieceTableHelper.getBuffer pt p.sourcelet sliceStart := p.start + (readStart - pStart)let sliceLen := readEnd - readStartlet cnt := ViE.Unicode.countChars buf sliceStart sliceLenscan (i + 1) pEnd (acc + cnt)scan 0 currentOff 0| internal children _ =>let rec scanInternal (i : Nat) (off : Nat) (acc : Nat) : Nat :=if i >= children.size then accelselet c := children[i]!let s := traverse c offscanInternal (i + 1) (off + c.length) (acc + s)scanInternal 0 currentOff 0traverse t 0
let c := children[i]!let cLen := length cif offset < accOffset + cLen thenlet (l, r) := split c (offset - accOffset) ptlet leftSide := mkInternal ((children.extract 0 i).push l)let rightSide := mkInternal (#[r] ++ (children.extract (i + 1) children.size))(leftSide, rightSide)elsefindSplitInternal (i + 1) (accOffset + cLen)findSplitInternal 0 0
/-- Get line char length (0-indexed). Excludes newline at end of line. -/def getLineLength (t : PieceTree) (lineIdx : Nat) (pt : PieceTable) : Option Nat :=let totalLines := t.lineBreaksif lineIdx > totalLines then noneelselet startOffset := if lineIdx == 0 then 0 else findNthNewline t (lineIdx - 1) pt + 1let endOffset :=if lineIdx == totalLines thent.lengthelsefindNthNewline t lineIdx ptsome (countCharsInRange t startOffset endOffset pt)
/-- Delete range from tree -/def delete (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable) : ViE.PieceTree :=let (l, mid_r) := split t offset ptlet (_, r) := split mid_r len ptconcat l r
def getLine (t : PieceTree) (lineIdx : Nat) (pt : PieceTable) : Option String :=let totalLines := t.lineBreaksif lineIdx > totalLines then noneelselet startOffset := if lineIdx == 0 then 0 else findNthNewline t (lineIdx - 1) pt + 1let endOffset :=if lineIdx == totalLines thent.lengthelsefindNthNewline t lineIdx ptsome (getSubstring t startOffset endOffset pt)
/-- Get substring from tree -/partial def getSubstring (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable) : String :=let rec collect (t : ViE.PieceTree) (off : Nat) (l : Nat) (acc : Array ByteArray) : (Array ByteArray × Nat) :=if l == 0 then (acc, 0)else match t with| ViE.PieceTree.empty => (acc, 0)| ViE.PieceTree.leaf pieces _ =>let rec scanLeaf (i : Nat) (accOffset : Nat) (currAcc : Array ByteArray) (remain : Nat) : (Array ByteArray × Nat) :=if i >= pieces.size || remain == 0 then (currAcc, l - remain)elselet p := pieces[i]!let pLen := p.lengthif off < accOffset + pLen thenlet pStart := if off > accOffset then off - accOffset else 0let readLen := min remain (pLen - pStart)let buf := PieceTableHelper.getBuffer pt p.sourcelet slice := buf.extract (p.start + pStart) (p.start + pStart + readLen)scanLeaf (i + 1) (accOffset + pLen) (currAcc.push slice) (remain - readLen)elsescanLeaf (i + 1) (accOffset + pLen) currAcc remainscanLeaf 0 0 acc l| ViE.PieceTree.internal children _ =>let rec scanInternal (i : Nat) (accOffset : Nat) (currAcc : Array ByteArray) (remain : Nat) : (Array ByteArray × Nat) :=if i >= children.size || remain == 0 then (currAcc, l - remain)elselet c := children[i]!let cLen := length cif off < accOffset + cLen thenlet cStart := if off > accOffset then off - accOffset else 0let (newAcc, readInThisChild) := collect c cStart remain currAccscanInternal (i + 1) (accOffset + cLen) newAcc (remain - readInThisChild)elsescanInternal (i + 1) (accOffset + cLen) currAcc remainscanInternal 0 0 acc llet (chunks, _) := collect t offset len #[]let combined := chunks.foldl (fun (acc : ByteArray) (b : ByteArray) => acc ++ b) (ByteArray.mk #[])String.fromUTF8! combined
/-- Get line range (start, length) -/def getLineRange (t : PieceTree) (lineIdx : Nat) (pt : PieceTable) : Option (Nat × Nat) :=let totalLines := t.lineBreaksif lineIdx > totalLines then noneelselet startOffset := if lineIdx == 0 then 0 else findNthNewline t (lineIdx - 1) pt + 1let endOffset :=if lineIdx == totalLines thent.lengthelsefindNthNewline t lineIdx ptsome (startOffset, endOffset - startOffset)
/-- Find the leaf and relative offset containing the Nth newline -/partial def findNthNewlineLeaf (t : ViE.PieceTree) (n : Nat) (pt : ViE.PieceTable) : Option (ViE.Piece × Nat × Nat) :=let rec scan (t : ViE.PieceTree) (n : Nat) (accOffset : Nat) : Option (ViE.Piece × Nat × Nat) :=match t with| ViE.PieceTree.empty => none| ViE.PieceTree.leaf pieces _ =>let rec findInPieces (i : Nat) (currN : Nat) (currOff : Nat) : Option (ViE.Piece × Nat × Nat) :=if i >= pieces.size then noneelselet p := pieces[i]!if currN < p.lineBreaks thenlet buf := PieceTableHelper.getBuffer pt p.sourcelet rec findOffset (j : Nat) (targetN : Nat) : Nat :=if j >= p.length then p.lengthelse if buf[p.start + j]! == 10 thenif targetN == 0 then j + 1else findOffset (j + 1) (targetN - 1)else findOffset (j + 1) targetNlet relOffset := findOffset 0 currNsome (p, currOff, relOffset)elsefindInPieces (i + 1) (currN - p.lineBreaks) (currOff + p.length)findInPieces 0 n accOffset| ViE.PieceTree.internal children _ =>let rec findInChildren (i : Nat) (currN : Nat) (currOff : Nat) : Option (ViE.Piece × Nat × Nat) :=if i >= children.size then noneelselet child := children[i]!let childLines := lineBreaks childif currN < childLines thenscan child currN currOffelsefindInChildren (i + 1) (currN - childLines) (currOff + length child)findInChildren 0 n accOffsetscan t n 0
/-- Build a tree from a list of pieces (Bottom-Up construction) -/partial def fromPieces (pieces : Array Piece) : PieceTree :=if pieces.isEmpty then empty
/-- Get range of a line in byte offsets -/def getLineRange (t : ViE.PieceTree) (lineIdx : Nat) (pt : ViE.PieceTable) : Option (Nat × Nat) :=if lineIdx == 0 thenlet start := 0let endOff := match findNthNewlineLeaf t 0 pt with| some (_, acc, rel) => acc + rel - 1| none => length tsome (start, endOff)
-- Step 1: Create Leaveslet rec mkLeaves (i : Nat) (acc : Array PieceTree) : Array PieceTree :=if i >= pieces.size then accelselet chunk := pieces.extract i (i + NodeCapacity)let leaf := mkLeaf chunkmkLeaves (i + NodeCapacity) (acc.push leaf)let leaves := mkLeaves 0 #[]-- Step 2: Build Internal Nodes recursivelylet rec buildLevel (nodes : Array PieceTree) : PieceTree :=if nodes.size == 1 thennodes[0]!elselet rec mkNextLevel (i : Nat) (acc : Array PieceTree) : Array PieceTree :=if i >= nodes.size then accelselet chunk := nodes.extract i (i + NodeCapacity)let node := mkInternal chunkmkNextLevel (i + NodeCapacity) (acc.push node)
match findNthNewlineLeaf t (lineIdx - 1) pt with| some (_, acc, rel) =>let start := acc + rellet endOff := match findNthNewlineLeaf t lineIdx pt with| some (_, acc2, rel2) => acc2 + rel2 - 1| none => length tsome (start, endOff - start)| none => none
/-- A node in the B+ Piece Tree -/inductive PieceTree where| empty| leaf (pieces : Array Piece) (stats : Stats)| internal (children : Array PieceTree) (stats : Stats)deriving Inhabited, Reprstructure PieceTable whereoriginal : ByteArrayaddBuffers : Array ByteArraytree : PieceTreeundoStack : List (PieceTree × Nat) := []redoStack : List (PieceTree × Nat) := []undoStackCount : Nat := 0redoStackCount : Nat := 0undoLimit : Nat := 100lastInsert : Option LastInsert := nonederiving Inhabited
def cmdWorkspace (args : List String) (state : EditorState) : IO EditorState :=match args with| ["open", path] => cmdCd [path] state| ["rename", name] =>return { state withworkspace := { state.workspace with name := name },message := s!"Workspace renamed to: {name}"}| _ => return { state with message := "Usage: :workspace <open|rename> <args>" }
| ["new"] =>let name := s!"Group {state.workgroups.size}"let nextBufId := state.workgroups.foldl (fun m g => max m g.nextBufferId) 0let newWg := createEmptyWorkgroup name nextBufIdlet newState := { state withworkgroups := state.workgroups.push newWg,currentGroup := state.workgroups.size -- switch to new one using the size before push}return { newState with message := s!"Created workgroup: {name}" }| ["new", name] =>let nextBufId := state.workgroups.foldl (fun m g => max m g.nextBufferId) 0let newWg := createEmptyWorkgroup name nextBufIdlet newState := { state withworkgroups := state.workgroups.push newWg,currentGroup := state.workgroups.size}return { newState with message := s!"Created workgroup: {name}" }| ["close"] =>if state.workgroups.size <= 1 thenreturn { state with message := "Cannot close the last workgroup" }elseif h_idx : state.currentGroup < state.workgroups.size thenlet newGroups := state.workgroups.eraseIdx state.currentGroup h_idxlet newIdx := if state.currentGroup >= newGroups.size then newGroups.size - 1 else state.currentGroupreturn { state withworkgroups := newGroups,currentGroup := newIdx,message := "Workgroup closed"}elsereturn { state with message := "Error: invalid workgroup index" }| ["rename", name] =>let current := state.workgroups[state.currentGroup]!let updated := { current with name := name }return { state withworkgroups := state.workgroups.set! state.currentGroup updated,message := s!"Workgroup renamed to: {name}"}| ["next"] =>let nextIdx := (state.currentGroup + 1) % state.workgroups.sizelet wg := state.workgroups[nextIdx]!return { state with currentGroup := nextIdx, message := s!"Switched to: {wg.name}" }| ["prev"] =>let prevIdx := if state.currentGroup == 0 then state.workgroups.size - 1 else state.currentGroup - 1let wg := state.workgroups[prevIdx]!return { state with currentGroup := prevIdx, message := s!"Switched to: {wg.name}" }
if num < 10 thenlet s' := state.switchToWorkgroup numreturn { s' with message := s!"Switched to workgroup {num}" }
if num < state.workgroups.size thenlet wg := state.workgroups[num]!return { state with currentGroup := num, message := s!"Switched to: {wg.name}" }
| [] => return { state with message := s!"Current workgroup: {state.currentGroup}" }| _ => return { state with message := "Usage: :wg [0-9]" }
| [] =>let wg := state.workgroups[state.currentGroup]!return { state with message := s!"Current workgroup: {wg.name} (index {state.currentGroup})" }| _ => return { state with message := "Usage: :wg <new|close|rename|next|prev|index> [args]" }
import ViE.State.Configimport ViE.Configimport ViE.Command.Implimport ViE.Key.Mapimport ViE.State.Editnamespace Test.BugReproductionopen ViEdef assert (msg : String) (cond : Bool) : IO Unit := doif cond thenIO.println s!"[PASS] {msg}"elseIO.println s!"[FAIL] {msg}"throw (IO.userError s!"Assertion failed: {msg}")-- Helper to construct a full Configdef makeTestConfig : Config := {settings := ViE.defaultConfigcommands := ViE.Command.defaultCommandMapbindings := ViE.Key.makeKeyMap ViE.Command.defaultCommandMap}-- Run a sequence of keysdef runKeys (startState : EditorState) (keys : List Key) : IO EditorState := dolet config := makeTestConfiglet mut s := startStatefor k in keys dos ← ViE.update config s kreturn sdef test : IO Unit := doIO.println "Starting Bug Reproduction Test..."let s := ViE.initialState-- Scenario: Insert, Undo, Insertlet s1 := s.insertChar 'a'let s1 := s1.commitEdit -- Force separate undo grouplet s2 := s1.insertChar 'b'-- Text: 'ab', Cursor: (0, 2)let s3 := s2.undo-- Text: 'a', Cursor should be (0, 1)let cursor := s3.getCursorif cursor.col.val != 1 thenIO.println s!"[FAIL] Undo cursor mismatch. Expected 1, got {cursor.col.val}"assert "Undo cursor" falseelseIO.println "[PASS] Undo cursor correct"let s4 := s3.insertChar 'c'-- Text: 'ac'let text := getLineFromBuffer s4.getActiveBuffer 0 |>.getD ""if text != "ac" thenIO.println s!"[FAIL] Insert after undo failed. Expected 'ac', got '{text}'"assert "Insert after undo" falseelseIO.println "[PASS] Insert after undo works"-- Scenario: Paste, Undo, Paste (checking grouping too, but focusing on cursor)-- Resetlet s := ViE.initialStatelet s := s.insertChar 'x'let s := s.yankCurrentLine -- Yank 'x\n'let s := s.pasteBelow -- Paste 'x\n' -> 'x\nx\n' ??-- PasteBelow pastes line.-- Scenario: x commandlet s := ViE.initialStatelet s := s.insertChar 'h'let s := s.insertChar 'e'let s := s.insertChar 'y'-- "hey"let s := (s.moveCursorLeft).moveCursorLeft -- At 'h' (0,0)? No: 3 -> 2 -> 1. 'e'-- "hey" cursor at 2 ('y'). Left -> 1 ('e'). Left -> 0 ('h').-- Actually moveCursorLeft from (0,3) -> (0,2) 'y'.-- Let's use setCursorlet s := s.setCursor (Point.make 0 1) -- 'e'let s := s.deleteCharAfterCursor -- Should delete 'e' -> "hy"let text := getLineFromBuffer s.getActiveBuffer 0 |>.getD ""if text != "hy" thenIO.println s!"[FAIL] 'x' command (deleteCharAfterCursor) failed. Expected 'hy', got '{text}'"assert "x command" falseelseIO.println "[PASS] 'x' command works"IO.println "Bug Reproduction Test Finished"end Test.BugReproduction
import ViE.Data.PieceTabledef main : IO Unit := dolet iterations := 50000let mut pt := ViE.PieceTable.fromString "Initial content\n"IO.println s!"Performing {iterations} insertions..."for i in [0:iterations] dopt := pt.insert pt.tree.length s!"line {i}\n" pt.tree.lengthif i % 1000 == 0 thenIO.println s!"Iteration {i}..."let tree := pt.treematch tree with| .empty => IO.println "Tree is empty"| .leaf ps _ => IO.println s!"Tree is a single leaf with {ps.size} pieces"| .internal cs s =>IO.println s!"Tree is internal with {cs.size} children at root"IO.println s!"Tree height: {s.height}"-- Check if children are also flatlet mut maxChildSize := 0for c in cs domatch c with| .internal cs2 _ => maxChildSize := max maxChildSize cs2.size| .leaf ps _ => maxChildSize := max maxChildSize ps.size| .empty => continueIO.println s!"Max child size at level 1: {maxChildSize}"if iterations > 0 thenlet start := ← IO.monoMsNowlet _ := pt.getLineRange (iterations - 1)let endT := ← IO.monoMsNowIO.println s!"Time to getLineRange for last line: {endT - start}ms"
import ViE.Data.PieceTablenamespace Test.PasteReproductiondef test : IO Unit := doIO.println "--- Test 1: Paste below last line (no trailing newline) ---"let pt := ViE.PieceTable.fromString "line 1"IO.println s!"Initial: [{pt.toString}]"-- Yank line 1 (manually simulating EditorState.yankCurrentLine)let line1 := pt.getLine 0 |>.getD ""let yanked := if line1.endsWith "\n" then line1 else line1 ++ "\n"IO.println s!"Yanked: [{yanked}]"-- Paste below line 0 (simulating EditorState.pasteBelow)let (off, text) := match pt.getOffsetFromPoint 1 0 with| some o => (o, yanked)| none =>let len := pt.lengthif len > 0 thenif !pt.endsWithNewline then (len, "\n" ++ yanked) else (len, yanked)else (0, yanked)let pt2 := pt.insert off text offIO.println s!"After paste:\n[{pt2.toString}]"IO.println s!"Line count: {pt2.lineCount}"for i in [:pt2.lineCount] doIO.println s!"Line {i}: [{pt2.getLine i |>.getD "NONE"}]"IO.println "\n--- Test 2: Paste below last line (with trailing newline) ---"let ptB := ViE.PieceTable.fromString "line 1\n"IO.println s!"Initial: [{ptB.toString}]"let line1B := ptB.getLine 0 |>.getD ""let yankedB := if line1B.endsWith "\n" then line1B else line1B ++ "\n"let (offB, textB) := match ptB.getOffsetFromPoint 1 0 with| some o => (o, yankedB)| none =>let len := ptB.lengthif len > 0 thenif !ptB.endsWithNewline then (len, "\n" ++ yankedB) else (len, yankedB)else (0, yankedB)let ptB2 := ptB.insert offB textB offBIO.println s!"After paste:\n[{ptB2.toString}]"IO.println s!"Line count: {ptB2.lineCount}"for i in [:ptB2.lineCount] doIO.println s!"Line {i}: [{ptB2.getLine i |>.getD "NONE"}]"
import ViE.State.Configimport ViE.Configimport ViE.Command.Implimport ViE.Key.Mapimport ViE.State.Editnamespace Test.CursorReproductionopen ViEdef assert (msg : String) (cond : Bool) : IO Unit := doif cond thenIO.println s!"[PASS] {msg}"elseIO.println s!"[FAIL] {msg}"throw (IO.userError s!"Assertion failed: {msg}")-- Helper to construct a full Configdef makeTestConfig : Config := {settings := ViE.defaultConfigcommands := ViE.Command.defaultCommandMapbindings := ViE.Key.makeKeyMap ViE.Command.defaultCommandMap}-- Run a sequence of keysdef runKeys (startState : EditorState) (keys : List Key) : IO EditorState := dolet config := makeTestConfiglet mut s := startStatefor k in keys dos ← ViE.update config s kreturn sdef test : IO Unit := doIO.println "Starting Cursor Reproduction Test..."let s := ViE.initialState-- Scenario: Insert, Undo, Insertlet s1 := s.insertChar 'a'let s1 := s1.commitEdit -- Force separate undo grouplet s2 := s1.insertChar 'b'-- Text: 'ab', Cursor: (0, 2)let s3 := s2.undo-- Text: 'a', Cursor should be (0, 1)let cursor := s3.getCursorif cursor.col.val != 1 thenIO.println s!"[FAIL] Undo cursor mismatch. Expected 1, got {cursor.col.val}"assert "Undo cursor" falseelseIO.println "[PASS] Undo cursor correct"let s4 := s3.insertChar 'c'-- Text: 'ac'let text := getLineFromBuffer s4.getActiveBuffer 0 |>.getD ""if text != "ac" thenIO.println s!"[FAIL] Insert after undo failed. Expected 'ac', got '{text}'"assert "Insert after undo" falseelseIO.println "[PASS] Insert after undo works"-- Scenario: Paste, Undo, Paste (checking grouping too, but focusing on cursor)-- Resetlet s := ViE.initialStatelet s := s.insertChar 'x'let s := s.yankCurrentLine -- Yank 'x\n'let _s := s.pasteBelow -- Paste 'x\n' -> 'x\nx\n' ??-- PasteBelow pastes line.-- Scenario: x commandlet s := ViE.initialStatelet s := s.insertChar 'h'let s := s.insertChar 'e'let s := s.insertChar 'y'-- "hey"let s := (s.moveCursorLeft).moveCursorLeft -- At 'h' (0,0)? No: 3 -> 2 -> 1. 'e'-- "hey" cursor at 2 ('y'). Left -> 1 ('e'). Left -> 0 ('h').-- Actually moveCursorLeft from (0,3) -> (0,2) 'y'.-- Let's use setCursorlet s := s.setCursor (Point.make 0 1) -- 'e'let s := s.deleteCharAfterCursor -- Should delete 'e' -> "hy"let text := getLineFromBuffer s.getActiveBuffer 0 |>.getD ""if text != "hy" thenIO.println s!"[FAIL] 'x' command (deleteCharAfterCursor) failed. Expected 'hy', got '{text}'"assert "x command" falseelseIO.println "[PASS] 'x' command works"IO.println "Cursor Reproduction Test Finished"end Test.CursorReproduction
import ViE.State.Configimport ViE.Configimport ViE.Command.Implimport ViE.Key.Mapimport ViE.State.Editimport ViE.UInamespace ViE.Benchmarkopen ViE/-- Mock Config for Benchmarking -/def makeBenchConfig : Config := {settings := ViE.defaultConfigcommands := ViE.Command.defaultCommandMapbindings := ViE.Key.makeKeyMap ViE.Command.defaultCommandMap}/-- Simulate a heavy editing session -/def runBenchmark (iterations : Nat) : IO Unit := dolet _config := makeBenchConfiglet mut s := ViE.initialState-- 1. Initial Large InsertionIO.println s!"Starting benchmark with {iterations} iterations..."for i in [0:iterations] dos := s.insertChar 'a'if i % 100 == 0 thens := s.commitEdit-- 2. Random Access / Movementfor _ in [0:iterations/10] dos := s.moveCursorUps := s.moveCursorLefts := s.insertChar 'b'-- 3. Clipboard (Yank / Paste)IO.println "Benchmarking Clipboard..."for _ in [0:iterations/100] dos := s.yankCurrentLines := s.pasteBelow-- 4. Workgroups (New / Switch / Close)IO.println "Benchmarking Workgroups..."for i in [0:iterations/500] dos := ← ViE.Command.cmdWg ["new", s!"BenchGroup {i}"] ss := s.insertChar 'w'-- Close them back (stress test closing)for _ in [0:iterations/500] dos := ← ViE.Command.cmdWg ["close"] s-- 5. Windows (Split / Cycle / Close)IO.println "Benchmarking Windows..."-- Note: Limit total windows to avoid extreme UI depth in benchmarkfor _ in [0:iterations/1000] dos := ViE.Window.splitWindow s true -- Vertical splits := ViE.Window.splitWindow s false -- Horizontal splits := s.insertChar 'v's := ViE.Window.cycleWindow s-- Close windowsfor _ in [0:iterations/500] dos := ViE.Window.closeActiveWindow s-- 6. Undo / Redo stressIO.println "Benchmarking Undo/Redo..."for _ in [0:iterations/20] dos := s.undo-- 7. Render Simulation (Crucial for B+ tree traversal check)-- We don't actually print to TTY to avoid I/O bottlenecks in perflet _ ← ViE.UI.render sIO.println "Benchmark completed."end ViE.Benchmarkdef main (args : List String) : IO Unit := dolet iter := args[0]? |>.bind String.toNat? |>.getD 1000ViE.Benchmark.runBenchmark iter