ITERATIONS=${1:-10000}

ITERATIONS=${1:-100}

./scripts/perf_profile.sh 10000
PERF_MODE=both ./scripts/perf_profile.sh 10000
PERF_MODE=c2c ./scripts/perf_profile.sh 10000

./scripts/perf_profile.sh
./scripts/perf_profile.sh 1000
PERF_MODE=both ./scripts/perf_profile.sh 1000
PERF_MODE=c2c ./scripts/perf_profile.sh 1000

Default iterations for `perf_profile.sh` is `100` when omitted.

/-- 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 + len
  let rec loop (i : Nat) (lines chars : Nat) : Nat × Nat :=
    if i >= stop then
      (lines, chars)
    else
      let b := bytes[i]!
      let lines' := if b == 10 then lines + 1 else lines
      let chars' := if (b &&& 0xC0) != 0x80 then chars + 1 else chars
      loop (i + 1) lines' chars'
  loop start 0 0

import ViE.UI.Syntax

      let syntaxSpans := ViE.UI.Syntax.highlightLine buf.filename lineStr

      let needsStyled := selRange.isSome || !searchMatches.isEmpty

      let needsStyled := selRange.isSome || !searchMatches.isEmpty || !syntaxSpans.isEmpty

        let mut styleActive := false

        let mut activeStyle : Option String := none

          if isSelected then
            if !styleActive then
              winBuf := winBuf.push "\x1b[7m"
              styleActive := true
          else if isMatched then
            if !styleActive then

          let desiredStyle : Option String :=
            if isSelected then
              some "\x1b[7m"
            else if isMatched then

                winBuf := winBuf.push state.config.searchHighlightCursorStyle

                some state.config.searchHighlightCursorStyle

                winBuf := winBuf.push state.config.searchHighlightStyle
              styleActive := true
          else if styleActive then
            winBuf := winBuf.push "\x1b[0m"
            styleActive := false

                some state.config.searchHighlightStyle
            else
              ViE.UI.Syntax.styleForByteRange syntaxSpans byteStart byteEnd
          if desiredStyle != activeStyle then
            match activeStyle with
            | some _ => winBuf := winBuf.push "\x1b[0m"
            | none => pure ()
            match desiredStyle with
            | some stl => winBuf := winBuf.push stl
            | none => pure ()
            activeStyle := desiredStyle

        if styleActive then

        if activeStyle.isSome then

    let lineIndex := ViE.Unicode.buildDisplayByteIndexWithTabStop raw st.config.tabStop
    let syntaxSpans := ViE.UI.Syntax.highlightLine buf.filename raw

      if hasSelection then

      if hasSelection || !syntaxSpans.isEmpty then

          let mut styleActive := false
          let mut dispCol := view.scrollCol.val

          let mut activeStyle : Option String := none
          let mut dispOffset := 0

            let dispCol := view.scrollCol.val + dispOffset
            let byteStart := ViE.Unicode.displayColToByteOffsetFromIndex lineIndex dispCol
            let byteEnd := ViE.Unicode.displayColToByteOffsetFromIndex lineIndex (dispCol + chW)

            if selected then
              if !styleActive then
                styled := styled.push "\x1b[7m"
                styleActive := true
            else if styleActive then
              styled := styled.push st.config.resetStyle
              styleActive := false

            let desiredStyle :=
              if selected then
                some "\x1b[7m"
              else
                ViE.UI.Syntax.styleForByteRange syntaxSpans byteStart byteEnd
            if desiredStyle != activeStyle then
              match activeStyle with
              | some _ => styled := styled.push st.config.resetStyle
              | none => pure ()
              match desiredStyle with
              | some stl => styled := styled.push stl
              | none => pure ()
              activeStyle := desiredStyle

            dispCol := dispCol + chW
          if styleActive then

            dispOffset := dispOffset + chW
          if activeStyle.isSome then

import ViE.Color
import ViE.UI.Search
namespace ViE.UI.Syntax
open ViE
inductive Language where
  | plain
  | lean
  | markdown
  deriving Repr, BEq, Inhabited
structure Span where
  startByte : Nat
  endByte : Nat
  style : String
  deriving Repr, BEq, Inhabited
def leanKeywordStyle : String := ViE.Color.toFg ViE.Color.Color.brightBlue
def leanCommentStyle : String := ViE.Color.toFg ViE.Color.Color.brightBlack
def leanStringStyle : String := ViE.Color.toFg ViE.Color.Color.brightGreen
def leanNumberStyle : String := ViE.Color.toFg ViE.Color.Color.brightMagenta
def markdownHeadingStyle : String := ViE.Color.toFg ViE.Color.Color.brightCyan
def markdownCodeStyle : String := ViE.Color.toFg ViE.Color.Color.brightYellow
def markdownLinkStyle : String := ViE.Color.toFg ViE.Color.Color.brightBlue
def markdownEmphasisStyle : String := ViE.Color.toFg ViE.Color.Color.brightMagenta
private def isAsciiLower (n : Nat) : Bool := 97 <= n && n <= 122
private def isAsciiUpper (n : Nat) : Bool := 65 <= n && n <= 90
private def isAsciiDigit (n : Nat) : Bool := 48 <= n && n <= 57
private def isIdentStart (b : UInt8) : Bool :=
  let n := b.toNat
  isAsciiLower n || isAsciiUpper n || n == 95
private def isIdentCont (b : UInt8) : Bool :=
  let n := b.toNat
  isIdentStart b || isAsciiDigit n || n == 39
private 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 .lean
      else if name.endsWith ".md" || name.endsWith ".markdown" then .markdown
      else .plain
private def tokenizeLean (line : String) : Array Span := Id.run do
  let bytes := line.toUTF8
  let n := bytes.size
  let mut spans : Array Span := #[]
  let mut i := 0
  while i < n do
    let b := bytes[i]!
    if b == 34 then
      let mut j := i + 1
      let mut escaped := false
      let mut closed := false
      while j < n && !closed do
        let c := bytes[j]!
        if escaped then
          escaped := false
          j := j + 1
        else if c == 92 then
          escaped := true
          j := j + 1
        else if c == 34 then
          closed := true
          j := j + 1
        else
          j := j + 1
      spans := spans.push { startByte := i, endByte := j, style := leanStringStyle }
      i := j
    else if i + 1 < n && bytes[i]! == 45 && bytes[i + 1]! == 45 then
      spans := spans.push { startByte := i, endByte := n, style := leanCommentStyle }
      i := n
    else if i + 1 < n && bytes[i]! == 47 && bytes[i + 1]! == 45 then
      spans := spans.push { startByte := i, endByte := n, style := leanCommentStyle }
      i := n
    else if isAsciiDigit b.toNat then
      let mut j := i + 1
      while j < n do
        let c := bytes[j]!.toNat
        if isAsciiDigit c || c == 95 || c == 46 || c == 120 || c == 111 || c == 98 ||
           (65 <= c && c <= 70) || (97 <= c && c <= 102) then
          j := j + 1
        else
          break
      spans := spans.push { startByte := i, endByte := j, style := leanNumberStyle }
      i := j
    else if isIdentStart b then
      let mut j := i + 1
      while j < n && isIdentCont (bytes[j]!) do
        j := j + 1
      let tok := String.fromUTF8! (bytes.extract i j)
      if leanKeywords.contains tok then
        spans := spans.push { startByte := i, endByte := j, style := leanKeywordStyle }
      i := j
    else
      i := i + 1
  return spans
private def isMarkdownHeading (bytes : ByteArray) : Bool := Id.run do
  let n := bytes.size
  let mut i := 0
  while i < n && bytes[i]! == 32 do
    i := i + 1
  if i >= n || bytes[i]! != 35 then
    return false
  let mut j := i
  while j < n && bytes[j]! == 35 do
    j := j + 1
  return j < n && bytes[j]! == 32
private 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 do
  let bytes := line.toUTF8
  let n := bytes.size
  if isMarkdownHeading bytes then
    return #[{ startByte := 0, endByte := n, style := markdownHeadingStyle }]
  if isMarkdownFence bytes then
    return #[{ startByte := 0, endByte := n, style := markdownCodeStyle }]
  let mut spans : Array Span := #[]
  let mut i := 0
  while i < n do
    if bytes[i]! == 96 then
      let mut j := i + 1
      while j < n && bytes[j]! != 96 do
        j := j + 1
      if j < n then
        spans := spans.push { startByte := i, endByte := j + 1, style := markdownCodeStyle }
        i := j + 1
      else
        i := i + 1
    else if bytes[i]! == 91 then
      let mut j := i + 1
      while j < n && bytes[j]! != 93 do
        j := j + 1
      if j + 1 < n && bytes[j]! == 93 && bytes[j + 1]! == 40 then
        let mut k := j + 2
        while k < n && bytes[k]! != 41 do
          k := k + 1
        if k < n then
          spans := spans.push { startByte := i, endByte := k + 1, style := markdownLinkStyle }
          i := k + 1
        else
          i := i + 1
      else
        i := i + 1
    else if bytes[i]! == 42 || bytes[i]! == 95 then
      let delim := bytes[i]!
      let mut j := i + 1
      while j < n && bytes[j]! != delim do
        j := j + 1
      if j < n && j > i + 1 then
        spans := spans.push { startByte := i, endByte := j + 1, style := markdownEmphasisStyle }
        i := j + 1
      else
        i := i + 1
    else
      i := i + 1
  return spans
def highlightLine (filename : Option String) (line : String) : Array Span :=
  match detectLanguage filename with
  | .plain => #[]
  | .lean => tokenizeLean line
  | .markdown => tokenizeMarkdown line
def styleForByteRange (spans : Array Span) (byteStart byteEnd : Nat) : Option String :=
  let rec loop (i : Nat) : Option String :=
    if i >= spans.size then
      none
    else
      let s := spans[i]!
      if overlapsByteRange (s.startByte, s.endByte) byteStart byteEnd then
        some s.style
      else
        loop (i + 1)
  loop 0
end ViE.UI.Syntax

              let stop := p.start + p.length
              let mut i := p.start

              let stop := p.start.toNat + p.length.toNat
              let mut i := p.start.toNat

        | PieceTree.internal children _ _ =>

        | PieceTree.internal children _ _ _ =>

    withLineIndexCache {

    {

      undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none

      undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none, lineIndexCache := some #[0]

    -- Split bytes into chunks to avoid monolithic pieces

    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 len
        let chars := Unicode.countChars bytes start len
        let piece : Piece := { source := BufferSource.original, start := start, length := len, lineBreaks := lines, charCount := chars }
        splitChunks (start + len) (acc.push piece)

        let stop := start + len
        let rec scan (i : Nat) (lines chars : Nat) (lineStarts : Array Nat) : (Nat × Nat × Array Nat) :=
          if i >= stop then
            (lines, chars, lineStarts)
          else
            let b := bytes[i]!
            let lineStarts' := if b == 10 then lineStarts.push (i + 1) else lineStarts
            let lines' := if b == 10 then lines + 1 else lines
            let chars' := if (b &&& 0xC0) != 0x80 then chars + 1 else chars
            scan (i + 1) lines' chars' lineStarts'
        let (lines, chars, starts') := scan start 0 0 starts
        let piece : Piece := { source := BufferSource.original, start := start.toUInt64, length := len.toUInt64, lineBreaks := lines.toUInt64, charCount := chars.toUInt64 }
        splitChunks (start + len) (pieces.push piece) starts'

    let pieces := splitChunks 0 #[]

    let (pieces, starts) := splitChunks 0 #[] #[0]

    withLineIndexCache {

    {

      undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none

      undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none, lineIndexCache := some starts

def PieceTable.length (pt : PieceTable) : Nat := (PieceTree.stats pt.tree).bytes

def PieceTable.length (pt : PieceTable) : Nat := (PieceTree.stats pt.tree).bytes.toNat

      let lines := ViE.Unicode.countNewlines bytes start len
      let chars := ViE.Unicode.countChars bytes start len

      let (lines, chars) := ViE.Unicode.countNewlinesAndChars bytes start len

        start := startOff + start,
        length := len,
        lineBreaks := lines,
        charCount := chars

        start := (startOff + start).toUInt64,
        length := len.toUInt64,
        lineBreaks := lines.toUInt64,
        charCount := chars.toUInt64

def splitPiece (p : ViE.Piece) (offset : Nat) (pt : ViE.PieceTable) : (ViE.Piece × ViE.Piece) :=

def splitPiece (p : ViE.Piece) (offset : UInt64) (pt : ViE.PieceTable) : (ViE.Piece × ViE.Piece) :=

  let leftLines := ViE.Unicode.countNewlines buf p.start leftLen
  let leftChars := ViE.Unicode.countChars buf p.start leftLen

  let (leftLines, leftChars) := ViE.Unicode.countNewlinesAndChars buf p.start.toNat leftLen.toNat

  let leftPiece : ViE.Piece := { p with length := leftLen, lineBreaks := leftLines, charCount := leftChars }

  let leftPiece : ViE.Piece := { p with length := leftLen, lineBreaks := leftLines.toUInt64, charCount := leftChars.toUInt64 }

    start := p.start + leftLen,

    start := p.start + leftLen

    lineBreaks := p.lineBreaks - leftLines,
    charCount := p.charCount - leftChars

    lineBreaks := p.lineBreaks - leftLines.toUInt64,
    charCount := p.charCount - leftChars.toUInt64

  | ViE.PieceTree.internal _ s _ => s

  | ViE.PieceTree.internal _ s _ _ => s

def length (t : ViE.PieceTree) : Nat := (stats t).bytes
def lineBreaks (t : ViE.PieceTree) : Nat := (stats t).lines
def height (t : ViE.PieceTree) : Nat := (stats t).height

def length (t : ViE.PieceTree) : Nat := (stats t).bytes.toNat
def lineBreaks (t : ViE.PieceTree) : Nat := (stats t).lines.toNat
def 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 do
    let mut cumBytes : Array UInt64 := #[0]
    let mut cumLines : Array UInt64 := #[0]
    let mut cumChars : Array UInt64 := #[0]
    for i in [0:children.size] do
      let child := children[i]!
      let s := stats child
      let 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 do
    let arr := imeta.cumulativeBytes
    if arr.isEmpty then return 0
    if arr.size == 1 then return 0
    let mut left := 0
    let mut right := arr.size - 2  -- Last valid child index
    while left < right do
      let mid := (left + right + 1) / 2
      if arr[mid]! <= offset then
        left := mid
      else
        right := mid - 1
    return left
/-- Binary search to find child index containing the given line number -/
def findChildForLine (imeta : ViE.InternalMeta) (lineIdx : UInt64) : Nat :=
  Id.run do
    let arr := imeta.cumulativeLines
    if arr.isEmpty then return 0
    if arr.size == 1 then return 0
    let mut left := 0
    let mut right := arr.size - 2  -- Last valid child index
    while left < right do
      let mid := (left + right + 1) / 2
      if arr[mid]! <= lineIdx then
        left := mid
      else
        right := mid - 1

    return left

    let mask : UInt8 := UInt8.ofNat (1 <<< bitIdx)

    let mask : UInt8 := (1 : UInt8) <<< bitIdx.toUInt8

    let mask : UInt8 := UInt8.ofNat (1 <<< bitIdx)

    let mask : UInt8 := (1 : UInt8) <<< bitIdx.toUInt8

/-- Polynomial rolling hash with base 31: b0·31² + b1·31¹ + b2·31⁰.
    Used as the first hash function for Bloom filter double-hashing. -/

/-- Polynomial rolling hash with base 131: b0·131² + b1·131¹ + b2·131⁰.
    Used as the second hash function for Bloom filter double-hashing. -/

/-- Add a trigram to the Bloom filter. -/

    let slice := buf.extract p.start (p.start + p.length)

    let slice := buf.extract p.start.toNat (p.start.toNat + p.length.toNat)

    let slice := buf.extract p.start (p.start + p.length)

    let slice := buf.extract p.start.toNat (p.start.toNat + p.length.toNat)

      let slice := buf.extract p.start (p.start + p.length)

      let slice := buf.extract p.start.toNat (p.start.toNat + p.length.toNat)

  let s := pieces.foldl (fun acc p => acc + (ViE.Stats.ofPiece p)) ViE.Stats.empty
  let searchMeta := buildBloomForPieces pieces pt
  ViE.PieceTree.leaf pieces s searchMeta

  if pieces.size == 0 then
    ViE.PieceTree.empty
  else
    let s := pieces.foldl (fun acc p => acc + (ViE.Stats.ofPiece p)) ViE.Stats.empty
    let searchMeta := buildBloomForPieces pieces pt
    ViE.PieceTree.leaf pieces s searchMeta

  let s := children.foldl (fun acc c => acc + (stats c)) ViE.Stats.empty
  let s := { s with height := s.height + 1 }
  let searchMeta := buildBloomForChildren children
  ViE.PieceTree.internal children s searchMeta

  let validChildren := children.filter (fun c => match c with | ViE.PieceTree.empty => false | _ => true)
  if validChildren.size == 0 then
    ViE.PieceTree.empty
  else
    let s := validChildren.foldl (fun acc c => acc + (stats c)) ViE.Stats.empty
    let s := { s with height := s.height + 1 }
    let searchMeta := buildBloomForChildren validChildren
    let internalMeta := computeCumulativeOffsets validChildren
    ViE.PieceTree.internal validChildren s searchMeta internalMeta

        | ViE.PieceTree.internal children _ _ =>

        | ViE.PieceTree.internal children _ _ _ =>

/-- 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 right
    let mut frames : Array (Array ViE.PieceTree) := #[]  -- left siblings at each level
    let mut cur := tree
    while height cur > targetHeight do
      match cur with
      | ViE.PieceTree.internal children _ _ _ =>
          -- Save all children except the rightmost as left siblings
          frames := 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 children
    let mut newChildren : Array ViE.PieceTree := #[cur, node]
    -- Walk back up, rebuilding from frames
    let mut fi := frames.size
    while fi > 0 do
      let j := fi - 1
      let siblings := frames[j]!
      let combined := siblings ++ newChildren
      if combined.size <= ViE.NodeCapacity then
        newChildren := #[mkInternal combined]
      else
        -- Split: too many children
        let mid := combined.size / 2
        let leftNode := mkInternal (combined.extract 0 mid)
        let rightNode := mkInternal (combined.extract mid combined.size)
        newChildren := #[leftNode, rightNode]
      fi := j
    if newChildren.size == 1 then
      return newChildren[0]!
    else
      return 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 left
    let mut frames : Array (Array ViE.PieceTree) := #[]  -- right siblings at each level
    let mut cur := tree
    while height cur > targetHeight do
      match cur with
      | ViE.PieceTree.internal children _ _ _ =>
          -- Save all children except the leftmost as right siblings
          frames := frames.push (children.extract 1 children.size)
          cur := children[0]!
      | _ => break
    -- cur and node are both at targetHeight; propagate them upward as new children
    let mut newChildren : Array ViE.PieceTree := #[node, cur]
    -- Walk back up, rebuilding from frames
    let mut fi := frames.size
    while fi > 0 do
      let j := fi - 1
      let siblings := frames[j]!
      let combined := newChildren ++ siblings
      if combined.size <= ViE.NodeCapacity then
        newChildren := #[mkInternal combined]
      else
        let mid := combined.size / 2
        let leftNode := mkInternal (combined.extract 0 mid)
        let rightNode := mkInternal (combined.extract mid combined.size)
        newChildren := #[leftNode, rightNode]
      fi := j
    if newChildren.size == 1 then
      return newChildren[0]!
    else
      return 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 node
    at 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 l
      let rh := height r
      if lh == rh then
        -- Same height: merge children to avoid unnecessary height increase
        match l, r with
        | ViE.PieceTree.internal cl _ _ _, ViE.PieceTree.internal cr _ _ _ =>
            let combined := cl ++ cr
            if combined.size <= ViE.NodeCapacity then
              mkInternal combined
            else
              let mid := combined.size / 2
              mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]
        | _, _ =>
            -- leaf + internal at same height (shouldn't normally happen), safe fallback
            insertRight l r rh
      else if lh > rh then
        -- l is taller: walk down l's right spine to find insertion point for r
        insertRight l r rh
      else
        -- r is taller: walk down r's left spine to find insertion point for l
        insertLeft l r lh

    let mut off := offset

    let mut off : UInt64 := offset.toUInt64

          let mut accOffset := 0

          let mut accOffset : UInt64 := 0

      | ViE.PieceTree.internal children _ _ =>
          let mut i := 0
          let mut accOffset := 0
          let mut found := false
          while i < children.size && !found do
            let c := children[i]!
            let cLen := length c
            if off < accOffset + cLen then
              frames := frames.push (children.extract 0 i, children.extract (i + 1) children.size)
              node := c
              off := off - accOffset
              found := true
            else
              accOffset := accOffset + cLen
              i := i + 1
          if !found then
            return (t, ViE.PieceTree.empty)

      | ViE.PieceTree.internal children _ _ imeta =>
          -- Use binary search to find the child containing the offset
          let childIdx := findChildForOffset imeta off
          let child := children[childIdx]!
          let childStart := imeta.cumulativeBytes[childIdx]!
          let relativeOffset := off - childStart
          frames := frames.push (children.extract 0 childIdx, children.extract (childIdx + 1) children.size)
          node := child
          off := relativeOffset
          -- Continue to next iteration

                    let pLen := p.length.toNat

                    let pEnd := pieceBase + p.length

                    let pEnd := pieceBase + pLen

                      let maxReadable := p.length - startInPiece

                      let maxReadable := pLen - startInPiece

                          out := out.push (buf[p.start + startInPiece + r]!)

                          out := out.push (buf[p.start.toNat + startInPiece + r]!)

                    pieceBase := pieceBase + p.length

                    pieceBase := pieceBase + pLen

              | ViE.PieceTree.internal children _ _ =>
                  let mut i := children.size
                  let mut childEnd := nodeEnd
                  while i > 0 do

              | ViE.PieceTree.internal children _ _ imeta =>
                  -- Use binary search to find start and end child indices
                  let relCursor : UInt64 := (if cursor > baseOffset then cursor - baseOffset else 0).toUInt64
                  let relEnd : UInt64 := (if endOffset > baseOffset then min (endOffset - baseOffset) (nodeLen - 1) else 0).toUInt64
                  let startChildIdx := findChildForOffset imeta relCursor
                  let endChildIdx := findChildForOffset imeta relEnd
                  -- Only process children in the relevant range
                  let mut i := min (endChildIdx + 1) children.size
                  while i > startChildIdx do

                    let childLen := length child
                    let childStart := childEnd - childLen

                    let childStart := baseOffset + imeta.cumulativeBytes[j]!.toNat
                    let childEnd := if j + 1 < imeta.cumulativeBytes.size
                                    then baseOffset + imeta.cumulativeBytes[j + 1]!.toNat
                                    else nodeEnd

                    childEnd := childStart

            if currN < p.lineBreaks then

            if currN < p.lineBreaks.toNat then

              let mut relOffset := p.length

              let pLen := p.length.toNat
              let mut relOffset := pLen

              while j < p.length && !done do
                if buf[p.start + j]! == 10 then

              while j < pLen && !done do
                if buf[p.start.toNat + j]! == 10 then

            currN := currN - p.lineBreaks
            currOff := currOff + p.length

            currN := currN - p.lineBreaks.toNat
            currOff := currOff + p.length.toNat

      | ViE.PieceTree.internal children _ _ =>

      | ViE.PieceTree.internal children _ _ _ =>

                | ViE.PieceTree.internal children _ m =>

                | ViE.PieceTree.internal children _ m _ =>

                | ViE.PieceTree.internal children _ m =>

                | ViE.PieceTree.internal children _ m _ =>

  start : Nat
  length : Nat
  lineBreaks : Nat
  charCount : Nat

  start : UInt64
  length : UInt64
  lineBreaks : UInt64
  charCount : UInt64

  bytes : Nat
  lines : Nat
  chars : Nat
  height : Nat

  bytes : UInt64
  lines : UInt64
  chars : UInt64
  height : UInt64

    height := max a.height b.height

    height := if a.height > b.height then a.height else b.height

/-- 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 UInt64
  deriving Inhabited, Repr

def InternalMeta.empty : InternalMeta := {
  cumulativeBytes := #[0],
  cumulativeLines := #[0],
  cumulativeChars := #[0]
}

  | internal (children : Array PieceTree) (stats : Stats) (searchMeta : SearchBloom)

  | internal (children : Array PieceTree) (stats : Stats) (searchMeta : SearchBloom) (internalMeta : InternalMeta)

  start : Nat
  length : Nat
  lineBreaks : Nat
  charCount : Nat

  start : UInt64
  length : UInt64
  lineBreaks : UInt64
  charCount : UInt64

  bytes : Nat
  lines : Nat
  chars : Nat
  height : Nat

  bytes : UInt64
  lines : UInt64
  chars : UInt64
  height : UInt64

    height := max a.height b.height

    height := if a.height > b.height then a.height else b.height

import Test.SyntaxHighlight

  Test.SyntaxHighlight.test

    | .internal cs _ _ => 1 + countNodesList cs.toList

    | .internal cs _ _ _ => 1 + countNodesList cs.toList

    | .internal cs _ _ => countLeavesList cs.toList

    | .internal cs _ _ _ => countLeavesList cs.toList

    | .internal cs _ _ => maxLeafPiecesList cs.toList

    | .internal cs _ _ _ => maxLeafPiecesList cs.toList

    | .internal cs _ _ =>

    | .internal cs _ _ _ =>

  | .internal cs _ _ => IO.println s!"root=internal children={cs.size}"

  | .internal cs _ _ _ => IO.println s!"root=internal children={cs.size}"

import ViE.UI.Syntax
import ViE.UI.Search
import Test.Utils
open Test.Utils
namespace Test.SyntaxHighlight
private def firstRangeOf (line : String) (pat : String) : Option (Nat × Nat) :=
  (ViE.UI.findAllMatchesBytes line.toUTF8 pat.toUTF8)[0]?
def testLean : IO Unit := do
  let line := "def x := 42 -- comment"
  let spans := ViE.UI.Syntax.highlightLine (some "Main.lean") line
  let (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 := do
  let line := "Use `code` and [link](url)"
  let spans := ViE.UI.Syntax.highlightLine (some "README.md") line
  let (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 := do
  IO.println "Starting SyntaxHighlight Test..."
  testLean
  testMarkdown
  IO.println "SyntaxHighlight Test passed!"
end Test.SyntaxHighlight

def testYankPasteClearing : IO Unit := do
  IO.println "testYankPasteClearing (yy+p reproduction)..."
  -- Simulate: insert 25 'i' chars + newline, then yy+p 4000 times
  let initLine := String.ofList (List.replicate 25 'i') ++ "\n"
  let lineBytes := initLine.toUTF8.size  -- 26 bytes
  let mut pt := PieceTable.fromString initLine
  let 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 pt
    match 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 pt
        if yankedBytes.size == 0 then
          throw <| 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 + 1
        let insertOffset := min insertOffset pt.length
        let yankStr := (String.fromUTF8! yankedBytes) ++ "\n"
        pt := pt.insert insertOffset yankStr insertOffset
        -- 3. Move cursor to pasted line
        cursorLine := cursorLine + 1
    -- 4. Verify tree length
    let expectedLen := lineBytes * (step + 2)
    let actualLen := pt.length
    if actualLen != expectedLen then
      throw <| IO.userError s!"[YankPaste] Length mismatch at step {step}: expected={expectedLen} actual={actualLen}"
    -- 5. Full consistency check every 500 steps
    if step % 500 == 0 then
      let rendered := pt.toString.toUTF8.size
      if rendered != expectedLen then
        throw <| 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"

  testYankPasteClearing

      start := i
      length := 1
      lineBreaks := 0
      charCount := 1 }

      start := i.toUInt64
      length := (1 : UInt64)
      lineBreaks := (0 : UInt64)
      charCount := (1 : UInt64) }

/-- Simple timer helper -/

/-- Generate large text content of specified size (in bytes). -/
def buildLargeText (sizeBytes : Nat) : String :=
  let lineLen := 80
  let line := String.ofList (List.replicate lineLen 'a') ++ "\n"
  let lineBytes := line.utf8ByteSize
  let numLines := sizeBytes / lineBytes
  String.intercalate "" (List.replicate numLines line)
/-- Case: Load large file (1MB). -/
def benchLoadLarge1MB (buildLeafBits : Bool) : IO Unit := do
  let text := buildLargeText (1024 * 1024)  -- 1MB
  let _ := PieceTable.fromString text buildLeafBits
  pure ()
/-- Case: Load large file (10MB). -/
def benchLoadLarge10MB (buildLeafBits : Bool) : IO Unit := do
  let text := buildLargeText (10 * 1024 * 1024)  -- 10MB
  let _ := PieceTable.fromString text buildLeafBits
  pure ()

/-- Case: Load large file (100MB). -/
def benchLoadLarge100MB (buildLeafBits : Bool) : IO Unit := do
  let text := buildLargeText (100 * 1024 * 1024)  -- 100MB
  let _ := PieceTable.fromString text buildLeafBits
  pure ()

/-- Case: Insert at middle of large file (1MB). -/
def benchInsertMidLarge1MB (iterations : Nat) (buildLeafBits : Bool) : IO Unit := do
  let text := buildLargeText (1024 * 1024)
  let pt := PieceTable.fromString text buildLeafBits
  let midOffset := pt.tree.stats.bytes.toNat / 2
  let mut checksum := 0
  -- Consume split results so optimizer cannot erase this loop.
  for _ in [0:iterations] do
    let (l, r) := PieceTree.split pt.tree midOffset pt
    checksum := checksum + l.stats.bytes.toNat + r.stats.bytes.toNat
  if checksum == 0 then
    IO.println "Zero bytes?"
/-- Case: Insert at middle of large file (10MB). -/
def benchInsertMidLarge10MB (iterations : Nat) (buildLeafBits : Bool) : IO Unit := do
  let text := buildLargeText (10 * 1024 * 1024)
  let pt := PieceTable.fromString text buildLeafBits
  let midOffset := pt.tree.stats.bytes.toNat / 2
  let mut checksum := 0
  -- Consume split results so optimizer cannot erase this loop.
  for _ in [0:iterations] do
    let (l, r) := PieceTree.split pt.tree midOffset pt
    checksum := checksum + l.stats.bytes.toNat + r.stats.bytes.toNat
  if checksum == 0 then
    IO.println "Zero bytes?"
/-- Case: Split operation on large file (1MB). -/
def benchSplitLarge1MB (iterations : Nat) (buildLeafBits : Bool) : IO Unit := do
  let text := buildLargeText (1024 * 1024)
  let pt := PieceTable.fromString text buildLeafBits
  let midOffset := pt.tree.stats.bytes.toNat / 2
  let mut checksum := 0
  for _ in [0:iterations] do
    let (l, r) := PieceTree.split pt.tree midOffset pt
    checksum := checksum + l.stats.bytes.toNat + r.stats.bytes.toNat
  if checksum == 0 then
    IO.println "Zero bytes?"
/-- Case: Split operation on large file (10MB). -/
def benchSplitLarge10MB (iterations : Nat) (buildLeafBits : Bool) : IO Unit := do
  let text := buildLargeText (10 * 1024 * 1024)
  let pt := PieceTable.fromString text buildLeafBits
  let midOffset := pt.tree.stats.bytes.toNat / 2
  let mut checksum := 0
  for _ in [0:iterations] do
    let (l, r) := PieceTree.split pt.tree midOffset pt
    checksum := checksum + l.stats.bytes.toNat + r.stats.bytes.toNat
  if checksum == 0 then
    IO.println "Zero bytes?"
/-- Case: GetBytes operation on large file (1MB). -/
def benchGetBytesLarge1MB (iterations : Nat) (buildLeafBits : Bool) : IO Unit := do
  let text := buildLargeText (1024 * 1024)
  let pt := PieceTable.fromString text buildLeafBits
  let chunkSize := 1024  -- 1KB chunks
  let mut checksum := 0
  for i in [0:iterations] do
    let offset := (i * chunkSize) % pt.tree.stats.bytes.toNat
    let bytes := PieceTree.getBytes pt.tree offset chunkSize pt
    checksum := checksum + bytes.size
  if checksum == 0 then
    IO.println "Zero bytes?"
/-- Case: GetBytes operation on large file (10MB). -/
def benchGetBytesLarge10MB (iterations : Nat) (buildLeafBits : Bool) : IO Unit := do
  let text := buildLargeText (10 * 1024 * 1024)
  let pt := PieceTable.fromString text buildLeafBits
  let chunkSize := 1024  -- 1KB chunks
  let mut checksum := 0
  for i in [0:iterations] do
    let offset := (i * chunkSize) % pt.tree.stats.bytes.toNat
    let bytes := PieceTree.getBytes pt.tree offset chunkSize pt
    checksum := checksum + bytes.size
  if checksum == 0 then
    IO.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] do
          let pt := PieceTable.fromString text buildLeafBits
          if 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] do
          let pt := PieceTable.fromString text buildLeafBits
          if 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] do
          let pt := PieceTable.fromString text buildLeafBits
          if 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)