A6E5SE5JPWUJJYIUS4CF7NMB5GM2SIIUXUZASSOVD467YWI5SCQQC KFKFELOTH4NL4DMXXWJ36OK62HWNJ7JJTHWA76CYHWGTGXMRGYFQC GUD2J453E3UTRJZIEEUUJ3ZIGL72ETUXTO57XQIZ2Y3ZU3C2R55QC KJLCU4X5Z3CZM4AORMWIKOPBWPVTDMLK4LYH7UXBJFUGL7AUQCSQC NBG3GUEJJMWS2FRJDU26KRQLA6O2YK77PDAPBMD3SKWLDTK23BVAC 6W6OJAUT3KLOXXKYR4GA3MG4ACLO2T4KX3SGD2KZDX6MYEZYTPHAC TKAAHADV62OQORAO7MYRRRHTGPMG3GKXU4Z4MFNLAO6DLTSDU3CAC ZL7ZSOEOGP2E24UEFC5VVPN5GTL3EUL34FA7F47WWWFPHJH2RS2AC TIAIRD7L5GWH22TOLDAGCIDCJDZ53YWK3KHQOH3EIU7RZEOEP32AC CNJGJCJZ6LRHHIRSRATSE3D3Z5OQGSSTDMXCPVXSKRQLYJFME6IAC 5SFTBD4FW6GQPKRUJBAII5R2EZPDYG6CH57BIJD4IVZBE6JZB2ZQC U45XPF3YKPXXRJ4MN24T2RV7GOL4FZKQSWX5P5I7WT4HC5XF4FHAC 32SDOYNGPOAAMEQMZLZUE3XE6D5CFSZU6M3JDRERUVPAB4TLZOOAC 25KGF2W2ORVH3Z7RIBDBRKILMM624MNHIMN5QXNMZOWQ5DOJUCZAC ./scripts/perf_profile.sh 10000PERF_MODE=both ./scripts/perf_profile.sh 10000PERF_MODE=c2c ./scripts/perf_profile.sh 10000
./scripts/perf_profile.sh./scripts/perf_profile.sh 1000PERF_MODE=both ./scripts/perf_profile.sh 1000PERF_MODE=c2c ./scripts/perf_profile.sh 1000
/-- Count newlines and UTF-8 characters in a byte array range in one pass. -/def countNewlinesAndChars (bytes : ByteArray) (start len : Nat) : Nat × Nat :=let stop := start + lenlet rec loop (i : Nat) (lines chars : Nat) : Nat × Nat :=if i >= stop then(lines, chars)elselet b := bytes[i]!let lines' := if b == 10 then lines + 1 else lineslet chars' := if (b &&& 0xC0) != 0x80 then chars + 1 else charsloop (i + 1) lines' chars'loop start 0 0
winBuf := winBuf.push state.config.searchHighlightStylestyleActive := trueelse if styleActive thenwinBuf := winBuf.push "\x1b[0m"styleActive := false
some state.config.searchHighlightStyleelseViE.UI.Syntax.styleForByteRange syntaxSpans byteStart byteEndif desiredStyle != activeStyle thenmatch activeStyle with| some _ => winBuf := winBuf.push "\x1b[0m"| none => pure ()match desiredStyle with| some stl => winBuf := winBuf.push stl| none => pure ()activeStyle := desiredStyle
if selected thenif !styleActive thenstyled := styled.push "\x1b[7m"styleActive := trueelse if styleActive thenstyled := styled.push st.config.resetStylestyleActive := false
let desiredStyle :=if selected thensome "\x1b[7m"elseViE.UI.Syntax.styleForByteRange syntaxSpans byteStart byteEndif desiredStyle != activeStyle thenmatch activeStyle with| some _ => styled := styled.push st.config.resetStyle| none => pure ()match desiredStyle with| some stl => styled := styled.push stl| none => pure ()activeStyle := desiredStyle
import ViE.Colorimport ViE.UI.Searchnamespace ViE.UI.Syntaxopen ViEinductive Language where| plain| lean| markdownderiving Repr, BEq, Inhabitedstructure Span wherestartByte : NatendByte : Natstyle : Stringderiving Repr, BEq, Inhabiteddef leanKeywordStyle : String := ViE.Color.toFg ViE.Color.Color.brightBluedef leanCommentStyle : String := ViE.Color.toFg ViE.Color.Color.brightBlackdef leanStringStyle : String := ViE.Color.toFg ViE.Color.Color.brightGreendef leanNumberStyle : String := ViE.Color.toFg ViE.Color.Color.brightMagentadef markdownHeadingStyle : String := ViE.Color.toFg ViE.Color.Color.brightCyandef markdownCodeStyle : String := ViE.Color.toFg ViE.Color.Color.brightYellowdef markdownLinkStyle : String := ViE.Color.toFg ViE.Color.Color.brightBluedef markdownEmphasisStyle : String := ViE.Color.toFg ViE.Color.Color.brightMagentaprivate def isAsciiLower (n : Nat) : Bool := 97 <= n && n <= 122private def isAsciiUpper (n : Nat) : Bool := 65 <= n && n <= 90private def isAsciiDigit (n : Nat) : Bool := 48 <= n && n <= 57private def isIdentStart (b : UInt8) : Bool :=let n := b.toNatisAsciiLower n || isAsciiUpper n || n == 95private def isIdentCont (b : UInt8) : Bool :=let n := b.toNatisIdentStart b || isAsciiDigit n || n == 39private def leanKeywords : Array String := #["abbrev", "axiom", "by", "class", "constant", "def", "deriving", "do","else", "end", "example", "from", "have", "if", "import", "in", "inductive","instance", "let", "match", "mutual", "namespace", "open", "opaque", "private","protected", "set_option", "show", "structure", "syntax", "termination_by","theorem", "unsafe", "variable", "where", "with"]def detectLanguage (filename : Option String) : Language :=match filename with| none => .plain| some name =>if name.endsWith ".lean" then .leanelse if name.endsWith ".md" || name.endsWith ".markdown" then .markdownelse .plainprivate def tokenizeLean (line : String) : Array Span := Id.run dolet bytes := line.toUTF8let n := bytes.sizelet mut spans : Array Span := #[]let mut i := 0while i < n dolet b := bytes[i]!if b == 34 thenlet mut j := i + 1let mut escaped := falselet mut closed := falsewhile j < n && !closed dolet c := bytes[j]!if escaped thenescaped := falsej := j + 1else if c == 92 thenescaped := truej := j + 1else if c == 34 thenclosed := truej := j + 1elsej := j + 1spans := spans.push { startByte := i, endByte := j, style := leanStringStyle }i := jelse if i + 1 < n && bytes[i]! == 45 && bytes[i + 1]! == 45 thenspans := spans.push { startByte := i, endByte := n, style := leanCommentStyle }i := nelse if i + 1 < n && bytes[i]! == 47 && bytes[i + 1]! == 45 thenspans := spans.push { startByte := i, endByte := n, style := leanCommentStyle }i := nelse if isAsciiDigit b.toNat thenlet mut j := i + 1while j < n dolet c := bytes[j]!.toNatif isAsciiDigit c || c == 95 || c == 46 || c == 120 || c == 111 || c == 98 ||(65 <= c && c <= 70) || (97 <= c && c <= 102) thenj := j + 1elsebreakspans := spans.push { startByte := i, endByte := j, style := leanNumberStyle }i := jelse if isIdentStart b thenlet mut j := i + 1while j < n && isIdentCont (bytes[j]!) doj := j + 1let tok := String.fromUTF8! (bytes.extract i j)if leanKeywords.contains tok thenspans := spans.push { startByte := i, endByte := j, style := leanKeywordStyle }i := jelsei := i + 1return spansprivate def isMarkdownHeading (bytes : ByteArray) : Bool := Id.run dolet n := bytes.sizelet mut i := 0while i < n && bytes[i]! == 32 doi := i + 1if i >= n || bytes[i]! != 35 thenreturn falselet mut j := iwhile j < n && bytes[j]! == 35 doj := j + 1return j < n && bytes[j]! == 32private def isMarkdownFence (bytes : ByteArray) : Bool :=(bytes.size >= 3 && bytes[0]! == 96 && bytes[1]! == 96 && bytes[2]! == 96) ||(bytes.size >= 3 && bytes[0]! == 126 && bytes[1]! == 126 && bytes[2]! == 126)private def tokenizeMarkdown (line : String) : Array Span := Id.run dolet bytes := line.toUTF8let n := bytes.sizeif isMarkdownHeading bytes thenreturn #[{ startByte := 0, endByte := n, style := markdownHeadingStyle }]if isMarkdownFence bytes thenreturn #[{ startByte := 0, endByte := n, style := markdownCodeStyle }]let mut spans : Array Span := #[]let mut i := 0while i < n doif bytes[i]! == 96 thenlet mut j := i + 1while j < n && bytes[j]! != 96 doj := j + 1if j < n thenspans := spans.push { startByte := i, endByte := j + 1, style := markdownCodeStyle }i := j + 1elsei := i + 1else if bytes[i]! == 91 thenlet mut j := i + 1while j < n && bytes[j]! != 93 doj := j + 1if j + 1 < n && bytes[j]! == 93 && bytes[j + 1]! == 40 thenlet mut k := j + 2while k < n && bytes[k]! != 41 dok := k + 1if k < n thenspans := spans.push { startByte := i, endByte := k + 1, style := markdownLinkStyle }i := k + 1elsei := i + 1elsei := i + 1else if bytes[i]! == 42 || bytes[i]! == 95 thenlet delim := bytes[i]!let mut j := i + 1while j < n && bytes[j]! != delim doj := j + 1if j < n && j > i + 1 thenspans := spans.push { startByte := i, endByte := j + 1, style := markdownEmphasisStyle }i := j + 1elsei := i + 1elsei := i + 1return spansdef highlightLine (filename : Option String) (line : String) : Array Span :=match detectLanguage filename with| .plain => #[]| .lean => tokenizeLean line| .markdown => tokenizeMarkdown linedef styleForByteRange (spans : Array Span) (byteStart byteEnd : Nat) : Option String :=let rec loop (i : Nat) : Option String :=if i >= spans.size thennoneelselet s := spans[i]!if overlapsByteRange (s.startByte, s.endByte) byteStart byteEnd thensome s.styleelseloop (i + 1)loop 0end ViE.UI.Syntax
let rec splitChunks (start : Nat) (acc : Array Piece) : Array Piece :=if start >= totalSize then acc
-- Split bytes into chunks while collecting line starts in one pass.let rec splitChunks (start : Nat) (pieces : Array Piece) (starts : Array Nat) : (Array Piece × Array Nat) :=if start >= totalSize then(pieces, starts)
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 }splitChunks (start + len) (acc.push piece)
let stop := start + lenlet rec scan (i : Nat) (lines chars : Nat) (lineStarts : Array Nat) : (Nat × Nat × Array Nat) :=if i >= stop then(lines, chars, lineStarts)elselet b := bytes[i]!let lineStarts' := if b == 10 then lineStarts.push (i + 1) else lineStartslet lines' := if b == 10 then lines + 1 else lineslet chars' := if (b &&& 0xC0) != 0x80 then chars + 1 else charsscan (i + 1) lines' chars' lineStarts'let (lines, chars, starts') := scan start 0 0 startslet piece : Piece := { source := BufferSource.original, start := start.toUInt64, length := len.toUInt64, lineBreaks := lines.toUInt64, charCount := chars.toUInt64 }splitChunks (start + len) (pieces.push piece) starts'
start := startOff + start,length := len,lineBreaks := lines,charCount := chars
start := (startOff + start).toUInt64,length := len.toUInt64,lineBreaks := lines.toUInt64,charCount := chars.toUInt64
let leftLines := ViE.Unicode.countNewlines buf p.start leftLenlet leftChars := ViE.Unicode.countChars buf p.start leftLen
let (leftLines, leftChars) := ViE.Unicode.countNewlinesAndChars buf p.start.toNat leftLen.toNat
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
def length (t : ViE.PieceTree) : Nat := (stats t).bytes.toNatdef lineBreaks (t : ViE.PieceTree) : Nat := (stats t).lines.toNatdef height (t : ViE.PieceTree) : Nat := (stats t).height.toNat
| ViE.PieceTree.internal _ _ m => m
| ViE.PieceTree.internal _ _ m _ => m/-- Compute cumulative offsets from children stats for O(log n) lookup -/def computeCumulativeOffsets (children : Array ViE.PieceTree) : ViE.InternalMeta :=Id.run dolet mut cumBytes : Array UInt64 := #[0]let mut cumLines : Array UInt64 := #[0]let mut cumChars : Array UInt64 := #[0]for i in [0:children.size] dolet child := children[i]!let s := stats childlet prevBytes := cumBytes.back!let prevLines := cumLines.back!let prevChars := cumChars.back!cumBytes := cumBytes.push (prevBytes + s.bytes)cumLines := cumLines.push (prevLines + s.lines)cumChars := cumChars.push (prevChars + s.chars)return {cumulativeBytes := cumBytes,cumulativeLines := cumLines,cumulativeChars := cumChars}/-- Binary search to find child index containing the given byte offset -/def findChildForOffset (imeta : ViE.InternalMeta) (offset : UInt64) : Nat :=Id.run dolet arr := imeta.cumulativeBytesif arr.isEmpty then return 0if arr.size == 1 then return 0let mut left := 0let mut right := arr.size - 2 -- Last valid child indexwhile left < right dolet mid := (left + right + 1) / 2if arr[mid]! <= offset thenleft := midelseright := mid - 1return left/-- Binary search to find child index containing the given line number -/def findChildForLine (imeta : ViE.InternalMeta) (lineIdx : UInt64) : Nat :=Id.run dolet arr := imeta.cumulativeLinesif arr.isEmpty then return 0if arr.size == 1 then return 0let mut left := 0let mut right := arr.size - 2 -- Last valid child indexwhile left < right dolet mid := (left + right + 1) / 2if arr[mid]! <= lineIdx thenleft := midelseright := mid - 1
let s := pieces.foldl (fun acc p => acc + (ViE.Stats.ofPiece p)) ViE.Stats.emptylet searchMeta := buildBloomForPieces pieces ptViE.PieceTree.leaf pieces s searchMeta
if pieces.size == 0 thenViE.PieceTree.emptyelselet s := pieces.foldl (fun acc p => acc + (ViE.Stats.ofPiece p)) ViE.Stats.emptylet searchMeta := buildBloomForPieces pieces ptViE.PieceTree.leaf pieces s searchMeta
let s := children.foldl (fun acc c => acc + (stats c)) ViE.Stats.emptylet s := { s with height := s.height + 1 }let searchMeta := buildBloomForChildren childrenViE.PieceTree.internal children s searchMeta
let validChildren := children.filter (fun c => match c with | ViE.PieceTree.empty => false | _ => true)if validChildren.size == 0 thenViE.PieceTree.emptyelselet s := validChildren.foldl (fun acc c => acc + (stats c)) ViE.Stats.emptylet s := { s with height := s.height + 1 }let searchMeta := buildBloomForChildren validChildrenlet internalMeta := computeCumulativeOffsets validChildrenViE.PieceTree.internal validChildren s searchMeta internalMeta
/-- Concatenate two trees while maintaining B+ tree invariants. -/
/-- Insert `node` into the right spine of `tree` at the level matching `targetHeight`.Returns the merged tree, handling overflow splits. -/private def insertRight (tree : ViE.PieceTree) (node : ViE.PieceTree) (targetHeight : Nat) : ViE.PieceTree :=Id.run do-- Collect spine frames going rightlet mut frames : Array (Array ViE.PieceTree) := #[] -- left siblings at each levellet mut cur := treewhile height cur > targetHeight domatch cur with| ViE.PieceTree.internal children _ _ _ =>-- Save all children except the rightmost as left siblingsframes := frames.push (children.extract 0 (children.size - 1))cur := children.back!| _ => break -- shouldn't happen if height > targetHeight-- cur and node are both at targetHeight; propagate them upward as new childrenlet mut newChildren : Array ViE.PieceTree := #[cur, node]-- Walk back up, rebuilding from frameslet mut fi := frames.sizewhile fi > 0 dolet j := fi - 1let siblings := frames[j]!let combined := siblings ++ newChildrenif combined.size <= ViE.NodeCapacity thennewChildren := #[mkInternal combined]else-- Split: too many childrenlet mid := combined.size / 2let leftNode := mkInternal (combined.extract 0 mid)let rightNode := mkInternal (combined.extract mid combined.size)newChildren := #[leftNode, rightNode]fi := jif newChildren.size == 1 thenreturn newChildren[0]!elsereturn mkInternal newChildren/-- Insert `node` into the left spine of `tree` at the level matching `targetHeight`.Returns the merged tree, handling overflow splits. -/private def insertLeft (node : ViE.PieceTree) (tree : ViE.PieceTree) (targetHeight : Nat) : ViE.PieceTree :=Id.run do-- Collect spine frames going leftlet mut frames : Array (Array ViE.PieceTree) := #[] -- right siblings at each levellet mut cur := treewhile height cur > targetHeight domatch cur with| ViE.PieceTree.internal children _ _ _ =>-- Save all children except the leftmost as right siblingsframes := frames.push (children.extract 1 children.size)cur := children[0]!| _ => break-- cur and node are both at targetHeight; propagate them upward as new childrenlet mut newChildren : Array ViE.PieceTree := #[node, cur]-- Walk back up, rebuilding from frameslet mut fi := frames.sizewhile fi > 0 dolet j := fi - 1let siblings := frames[j]!let combined := newChildren ++ siblingsif combined.size <= ViE.NodeCapacity thennewChildren := #[mkInternal combined]elselet mid := combined.size / 2let leftNode := mkInternal (combined.extract 0 mid)let rightNode := mkInternal (combined.extract mid combined.size)newChildren := #[leftNode, rightNode]fi := jif newChildren.size == 1 thenreturn newChildren[0]!elsereturn mkInternal newChildren/-- Concatenate two trees while maintaining B+ tree invariants.O(log n) structural merge: walks the spine of the taller tree to find a nodeat matching height, then inserts and propagates any overflows (splits) upward. -/
-- For mixed or internal trees, rebuild a balanced tree from in-order pieces.fromPieces (toPieces l ++ toPieces r) pt
let lh := height llet rh := height rif lh == rh then-- Same height: merge children to avoid unnecessary height increasematch l, r with| ViE.PieceTree.internal cl _ _ _, ViE.PieceTree.internal cr _ _ _ =>let combined := cl ++ crif combined.size <= ViE.NodeCapacity thenmkInternal combinedelselet mid := combined.size / 2mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]| _, _ =>-- leaf + internal at same height (shouldn't normally happen), safe fallbackinsertRight l r rhelse if lh > rh then-- l is taller: walk down l's right spine to find insertion point for rinsertRight l r rhelse-- r is taller: walk down r's left spine to find insertion point for linsertLeft l r lh
| ViE.PieceTree.internal children _ _ =>let mut i := 0let mut accOffset := 0let mut found := falsewhile i < children.size && !found dolet c := children[i]!let cLen := length cif off < accOffset + cLen thenframes := frames.push (children.extract 0 i, children.extract (i + 1) children.size)node := coff := off - accOffsetfound := trueelseaccOffset := accOffset + cLeni := i + 1if !found thenreturn (t, ViE.PieceTree.empty)
| ViE.PieceTree.internal children _ _ imeta =>-- Use binary search to find the child containing the offsetlet childIdx := findChildForOffset imeta offlet child := children[childIdx]!let childStart := imeta.cumulativeBytes[childIdx]!let relativeOffset := off - childStartframes := frames.push (children.extract 0 childIdx, children.extract (childIdx + 1) children.size)node := childoff := relativeOffset-- Continue to next iteration
| ViE.PieceTree.internal children _ _ =>let mut i := children.sizelet mut childEnd := nodeEndwhile i > 0 do
| ViE.PieceTree.internal children _ _ imeta =>-- Use binary search to find start and end child indiceslet relCursor : UInt64 := (if cursor > baseOffset then cursor - baseOffset else 0).toUInt64let relEnd : UInt64 := (if endOffset > baseOffset then min (endOffset - baseOffset) (nodeLen - 1) else 0).toUInt64let startChildIdx := findChildForOffset imeta relCursorlet endChildIdx := findChildForOffset imeta relEnd-- Only process children in the relevant rangelet mut i := min (endChildIdx + 1) children.sizewhile i > startChildIdx do
let childLen := length childlet childStart := childEnd - childLen
let childStart := baseOffset + imeta.cumulativeBytes[j]!.toNatlet childEnd := if j + 1 < imeta.cumulativeBytes.sizethen baseOffset + imeta.cumulativeBytes[j + 1]!.toNatelse nodeEnd
/-- Internal node metadata for O(log n) child lookup -/structure InternalMeta where/-- Cumulative byte offsets for each child (child[i] starts at cumulativeBytes[i]) -/cumulativeBytes : Array UInt64/-- Cumulative line counts for each child -/cumulativeLines : Array UInt64/-- Cumulative character counts for each child -/cumulativeChars : Array UInt64deriving Inhabited, Repr
import ViE.UI.Syntaximport ViE.UI.Searchimport Test.Utilsopen Test.Utilsnamespace Test.SyntaxHighlightprivate def firstRangeOf (line : String) (pat : String) : Option (Nat × Nat) :=(ViE.UI.findAllMatchesBytes line.toUTF8 pat.toUTF8)[0]?def testLean : IO Unit := dolet line := "def x := 42 -- comment"let spans := ViE.UI.Syntax.highlightLine (some "Main.lean") linelet (defS, defE) := (firstRangeOf line "def").getD (0, 0)let (numS, numE) := (firstRangeOf line "42").getD (0, 0)let (comS, comE) := (firstRangeOf line "-- comment").getD (0, 0)assertEqual "Lean keyword style" (some ViE.UI.Syntax.leanKeywordStyle) (ViE.UI.Syntax.styleForByteRange spans defS defE)assertEqual "Lean number style" (some ViE.UI.Syntax.leanNumberStyle) (ViE.UI.Syntax.styleForByteRange spans numS numE)assertEqual "Lean comment style" (some ViE.UI.Syntax.leanCommentStyle) (ViE.UI.Syntax.styleForByteRange spans comS comE)def testMarkdown : IO Unit := dolet line := "Use `code` and [link](url)"let spans := ViE.UI.Syntax.highlightLine (some "README.md") linelet (codeS, codeE) := (firstRangeOf line "`code`").getD (0, 0)let (linkS, linkE) := (firstRangeOf line "[link](url)").getD (0, 0)assertEqual "Markdown code style" (some ViE.UI.Syntax.markdownCodeStyle) (ViE.UI.Syntax.styleForByteRange spans codeS codeE)assertEqual "Markdown link style" (some ViE.UI.Syntax.markdownLinkStyle) (ViE.UI.Syntax.styleForByteRange spans linkS linkE)def test : IO Unit := doIO.println "Starting SyntaxHighlight Test..."testLeantestMarkdownIO.println "SyntaxHighlight Test passed!"end Test.SyntaxHighlight
def testYankPasteClearing : IO Unit := doIO.println "testYankPasteClearing (yy+p reproduction)..."-- Simulate: insert 25 'i' chars + newline, then yy+p 4000 timeslet initLine := String.ofList (List.replicate 25 'i') ++ "\n"let lineBytes := initLine.toUTF8.size -- 26 byteslet mut pt := PieceTable.fromString initLinelet mut cursorLine : Nat := 0
for step in [0:4000] do-- 1. yy: read current line content via getLineRange + getBytes (like real editor)let range := PieceTree.getLineRange pt.tree cursorLine ptmatch range with| none =>throw <| IO.userError s!"[YankPaste] getLineRange returned none at step {step}, line {cursorLine}"| some (off, len) =>let yankedBytes := PieceTree.getBytes pt.tree off len ptif yankedBytes.size == 0 thenthrow <| IO.userError s!"[YankPaste] Empty yank at step {step}, line {cursorLine}, off={off} len={len}"-- 2. p: paste below current line.-- Insert after end of current line (off + len + 1 for newline)let insertOffset := off + len + 1let insertOffset := min insertOffset pt.lengthlet yankStr := (String.fromUTF8! yankedBytes) ++ "\n"pt := pt.insert insertOffset yankStr insertOffset-- 3. Move cursor to pasted linecursorLine := cursorLine + 1-- 4. Verify tree lengthlet expectedLen := lineBytes * (step + 2)let actualLen := pt.lengthif actualLen != expectedLen thenthrow <| IO.userError s!"[YankPaste] Length mismatch at step {step}: expected={expectedLen} actual={actualLen}"-- 5. Full consistency check every 500 stepsif step % 500 == 0 thenlet rendered := pt.toString.toUTF8.sizeif rendered != expectedLen thenthrow <| IO.userError s!"[YankPaste] Rendered mismatch at step {step}: expected={expectedLen} rendered={rendered}"IO.println s!" step {step}: length={actualLen} lines={PieceTree.lineBreaks pt.tree} height={PieceTree.height pt.tree} OK"IO.println "[PASS] yank+paste 4000 iterations with getLineRange consistent"
/-- Generate large text content of specified size (in bytes). -/def buildLargeText (sizeBytes : Nat) : String :=let lineLen := 80let line := String.ofList (List.replicate lineLen 'a') ++ "\n"let lineBytes := line.utf8ByteSizelet numLines := sizeBytes / lineBytesString.intercalate "" (List.replicate numLines line)/-- Case: Load large file (1MB). -/def benchLoadLarge1MB (buildLeafBits : Bool) : IO Unit := dolet text := buildLargeText (1024 * 1024) -- 1MBlet _ := PieceTable.fromString text buildLeafBitspure ()/-- Case: Load large file (10MB). -/def benchLoadLarge10MB (buildLeafBits : Bool) : IO Unit := dolet text := buildLargeText (10 * 1024 * 1024) -- 10MBlet _ := PieceTable.fromString text buildLeafBitspure ()
/-- Case: Insert at middle of large file (1MB). -/def benchInsertMidLarge1MB (iterations : Nat) (buildLeafBits : Bool) : IO Unit := dolet text := buildLargeText (1024 * 1024)let pt := PieceTable.fromString text buildLeafBitslet midOffset := pt.tree.stats.bytes.toNat / 2let mut checksum := 0-- Consume split results so optimizer cannot erase this loop.for _ in [0:iterations] dolet (l, r) := PieceTree.split pt.tree midOffset ptchecksum := checksum + l.stats.bytes.toNat + r.stats.bytes.toNatif checksum == 0 thenIO.println "Zero bytes?"/-- Case: Insert at middle of large file (10MB). -/def benchInsertMidLarge10MB (iterations : Nat) (buildLeafBits : Bool) : IO Unit := dolet text := buildLargeText (10 * 1024 * 1024)let pt := PieceTable.fromString text buildLeafBitslet midOffset := pt.tree.stats.bytes.toNat / 2let mut checksum := 0-- Consume split results so optimizer cannot erase this loop.for _ in [0:iterations] dolet (l, r) := PieceTree.split pt.tree midOffset ptchecksum := checksum + l.stats.bytes.toNat + r.stats.bytes.toNatif checksum == 0 thenIO.println "Zero bytes?"/-- Case: Split operation on large file (1MB). -/def benchSplitLarge1MB (iterations : Nat) (buildLeafBits : Bool) : IO Unit := dolet text := buildLargeText (1024 * 1024)let pt := PieceTable.fromString text buildLeafBitslet midOffset := pt.tree.stats.bytes.toNat / 2let mut checksum := 0for _ in [0:iterations] dolet (l, r) := PieceTree.split pt.tree midOffset ptchecksum := checksum + l.stats.bytes.toNat + r.stats.bytes.toNatif checksum == 0 thenIO.println "Zero bytes?"/-- Case: Split operation on large file (10MB). -/def benchSplitLarge10MB (iterations : Nat) (buildLeafBits : Bool) : IO Unit := dolet text := buildLargeText (10 * 1024 * 1024)let pt := PieceTable.fromString text buildLeafBitslet midOffset := pt.tree.stats.bytes.toNat / 2let mut checksum := 0for _ in [0:iterations] dolet (l, r) := PieceTree.split pt.tree midOffset ptchecksum := checksum + l.stats.bytes.toNat + r.stats.bytes.toNatif checksum == 0 thenIO.println "Zero bytes?"/-- Case: GetBytes operation on large file (1MB). -/def benchGetBytesLarge1MB (iterations : Nat) (buildLeafBits : Bool) : IO Unit := dolet text := buildLargeText (1024 * 1024)let pt := PieceTable.fromString text buildLeafBitslet chunkSize := 1024 -- 1KB chunkslet mut checksum := 0for i in [0:iterations] dolet offset := (i * chunkSize) % pt.tree.stats.bytes.toNatlet bytes := PieceTree.getBytes pt.tree offset chunkSize ptchecksum := checksum + bytes.sizeif checksum == 0 thenIO.println "Zero bytes?"/-- Case: GetBytes operation on large file (10MB). -/def benchGetBytesLarge10MB (iterations : Nat) (buildLeafBits : Bool) : IO Unit := dolet text := buildLargeText (10 * 1024 * 1024)let pt := PieceTable.fromString text buildLeafBitslet chunkSize := 1024 -- 1KB chunkslet mut checksum := 0for i in [0:iterations] dolet offset := (i * chunkSize) % pt.tree.stats.bytes.toNatlet bytes := PieceTree.getBytes pt.tree offset chunkSize ptchecksum := checksum + bytes.sizeif checksum == 0 thenIO.println "Zero bytes?"
[ "insert", "edit", "clipboard", "workgroups", "windows", "undo", "search-bloom", "search-linear", "render" ]
[ "insert", "edit", "clipboard", "workgroups", "windows", "undo", "search-bloom", "search-linear", "render","load-1mb", "load-10mb", "load-100mb","insert-mid-1mb", "insert-mid-10mb","split-1mb", "split-10mb","getbytes-1mb", "getbytes-10mb" ]
| "load-1mb" =>let text := buildLargeText (1024 * 1024)timeCase "load-1mb" opts.iterations (for _ in [0:opts.iterations] dolet pt := PieceTable.fromString text buildLeafBitsif pt.tree.stats.bytes == 0 then IO.println "Zero bytes?" -- force usage)| "load-10mb" =>let text := buildLargeText (10 * 1024 * 1024)timeCase "load-10mb" opts.iterations (for _ in [0:opts.iterations] dolet pt := PieceTable.fromString text buildLeafBitsif pt.tree.stats.bytes == 0 then IO.println "Zero bytes?")| "load-100mb" =>let text := buildLargeText (100 * 1024 * 1024)timeCase "load-100mb" opts.iterations (for _ in [0:opts.iterations] dolet pt := PieceTable.fromString text buildLeafBitsif pt.tree.stats.bytes == 0 then IO.println "Zero bytes?")| "insert-mid-1mb" => timeCase "insert-mid-1mb" opts.iterations (benchInsertMidLarge1MB opts.iterations buildLeafBits)| "insert-mid-10mb" => timeCase "insert-mid-10mb" opts.iterations (benchInsertMidLarge10MB opts.iterations buildLeafBits)| "split-1mb" => timeCase "split-1mb" opts.iterations (benchSplitLarge1MB opts.iterations buildLeafBits)| "split-10mb" => timeCase "split-10mb" opts.iterations (benchSplitLarge10MB opts.iterations buildLeafBits)| "getbytes-1mb" => timeCase "getbytes-1mb" opts.iterations (benchGetBytesLarge1MB opts.iterations buildLeafBits)| "getbytes-10mb" => timeCase "getbytes-10mb" opts.iterations (benchGetBytesLarge10MB opts.iterations buildLeafBits)