def render (state : EditorState) : IO Unit := do

def render (state : EditorState) : IO EditorState := do
  if !state.dirty then return state

  let getBuffer (id : Nat) : FileBuffer :=
    wg.buffers.find? (fun b => b.id == id) |>.getD initialBuffer

  let getBuffer (st : EditorState) (id : Nat) : FileBuffer :=
    let wg := st.getCurrentWorkgroup
    wg.buffers.find? (fun b => b.id == id) |>.getD initialFileBuffer

  let rec renderLayout (l : Layout) (r c h w : Nat) : String := Id.run do

  let rec renderLayout (l : Layout) (st : EditorState) (r c h w : Nat) : (String × EditorState) := Id.run do

      let buf := getBuffer view.bufferId

      let buf := getBuffer st view.bufferId
      let mut currentSt := st

        let lineIdx := view.scrollRow + i

        let lineIdx : Row := ⟨view.scrollRow.val + i⟩

        if lineIdx < FileBuffer.lineCount buf then
           if let some lineStr := getLineFromBuffer buf lineIdx then
             let lnWidth := if state.config.showLineNumbers then 4 else 0
             let availableWidth := if w > lnWidth then w - lnWidth else 0

        if lineIdx.val < FileBuffer.lineCount buf then
           -- Check cache
           let cachedLine := buf.cache.find lineIdx
           let (displayLine, nextSt) := match cachedLine with
             | some s => (s, currentSt)
             | none =>
               if let some lineStr := getLineFromBuffer buf lineIdx then
                 let lnWidth := if st.config.showLineNumbers then 4 else 0
                 let availableWidth := if w > lnWidth then w - lnWidth else 0
                 let sub := lineStr.toRawSubstring.drop view.scrollCol.val
                 let dl := takeVisual sub availableWidth
                 -- Update cache in currentSt
                 let updatedBuf := { buf with cache := buf.cache.update lineIdx dl }
                 let s' := currentSt.updateCurrentWorkgroup fun wg =>
                   { wg with buffers := wg.buffers.map (fun (b : FileBuffer) => if b.id == buf.id then updatedBuf else b) }
                 (dl, s')
               else ("", currentSt)

             let sub := lineStr.toRawSubstring.drop view.scrollCol.val
             let displayLine := takeVisual sub availableWidth

           currentSt := nextSt
           if st.config.showLineNumbers then
             winBuf := winBuf ++ s!"{leftPad (toString (lineIdx.val + 1)) 3} "

             if state.config.showLineNumbers then
               winBuf := winBuf ++ s!"{leftPad (toString (lineIdx + 1)) 3} "

           let isVisual := st.mode == Mode.visual || st.mode == Mode.visualBlock
           let selRange := if isVisual then st.selectionStart else none

             let isVisual := state.mode == .visual || state.mode == .visualBlock
             let selRange := if isVisual then state.selectionStart else none

           match selRange with
           | none => winBuf := winBuf ++ displayLine
           | some _ =>
             let mut styleActive := false
             let chars := displayLine.toList
             let mut idx := 0
             for ch in chars do
                let colVal := view.scrollCol.val + idx
                let isSelected := st.isInSelection lineIdx ⟨colVal⟩

             match selRange with
             | none => winBuf := winBuf ++ displayLine
             | some _ =>
               let mut styleActive := false
               -- For highlighting, simpler to just iterate over result string or re-calculate
               -- This visual highlighting logic implies `displayLine` is the raw chars roughly.
               -- But `takeVisual` expands tabs/controls!
               -- Logic below assumes 1:1 char mapping which might be flawed if `takeVisual` changes string (e.g. ^A).
               -- Leaving visual highlight logic "as is" but it iterates `displayLine.toList`.
               -- `displayLine` is a String, so `toList` is fine (though allocs). Visual mode perf is secondary to normal nav.
               let chars := displayLine.toList
               let mut idx := 0
               for c in chars do
                  let col := view.scrollCol.val + idx
                  let isSelected := state.isInSelection lineIdx col
                  if isSelected && !styleActive then
                    winBuf := winBuf ++ "\x1b[7m" -- Inverse video
                    styleActive := true
                  else if !isSelected && styleActive then
                    winBuf := winBuf ++ "\x1b[0m"
                    styleActive := false

                if isSelected && !styleActive then
                  winBuf := winBuf ++ "\x1b[7m" -- Inverse video
                  styleActive := true
                else if !isSelected && styleActive then
                  winBuf := winBuf ++ "\x1b[0m"
                  styleActive := false

                  winBuf := winBuf ++ c.toString
                  idx := idx + 1

                winBuf := winBuf ++ ch.toString
                idx := idx + 1

               if styleActive then winBuf := winBuf ++ "\x1b[0m"

             if styleActive then winBuf := winBuf ++ "\x1b[0m"

           winBuf := winBuf ++ state.config.emptyLineMarker

           winBuf := winBuf ++ st.config.emptyLineMarker

        -- Clear the rest of the line to ensure clean overwrite

        -- Clear the rest of the line

      let modeStr := if id == wg.activeWindowId then s!"-- {state.mode} --" else "--"

      let modeStr := if id == currentSt.getCurrentWorkgroup.activeWindowId then s!"-- {st.mode} --" else "--"

      let statusStr := s!"{modeStr} {fileName}{eolMark} [W:{id} B:{view.bufferId}] [WG:{state.currentGroup}] {state.workspace.displayName}"
      -- Ensure status line also clears rest
      winBuf := winBuf ++ state.config.statusBarStyle ++ statusStr.trimAscii ++ Terminal.clearLineStr ++ state.config.resetStyle

      let statusStr := s!"{modeStr} {fileName}{eolMark} [W:{id} B:{view.bufferId}] [WG:{st.currentGroup}] {st.workspace.displayName}"
      winBuf := winBuf ++ st.config.statusBarStyle ++ statusStr.trimAscii ++ Terminal.clearLineStr ++ st.config.resetStyle

      -- Cursor drawing is separate (at end of frame)
      winBuf

      (winBuf, currentSt)

      let leftStr := renderLayout left r c h leftW

      let (leftStr, st') := renderLayout left st r c h leftW

           sepStr := sepStr ++ Terminal.moveCursorStr (r + i) sepCol ++ state.config.vSplitStr

           sepStr := sepStr ++ Terminal.moveCursorStr (r + i) sepCol ++ st.config.vSplitStr

      let rightStr := renderLayout right r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0)

      let (rightStr, st'') := renderLayout right st' r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0)

      leftStr ++ sepStr ++ rightStr

      (leftStr ++ sepStr ++ rightStr, st'')

      let topStr := renderLayout top r c topH w

      let (topStr, st') := renderLayout top st r c topH w

           sepStr := sepStr ++ state.config.hSplitStr

           sepStr := sepStr ++ st.config.hSplitStr

      let bottomStr := renderLayout bottom (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w

      let (bottomStr, st'') := renderLayout bottom st' (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w

      topStr ++ sepStr ++ bottomStr

      (topStr ++ sepStr ++ bottomStr, st'')

  buffer := buffer ++ renderLayout wg.layout 0 0 layoutH cols

  let (layoutStr, state) := renderLayout wg.layout state 0 0 layoutH cols
  buffer := buffer ++ layoutStr

         let buf := getBuffer view.bufferId

         let buf := getBuffer state view.bufferId

             if let some currentLineStr := getLineFromBuffer buf view.cursor.row.val then

             let rIdx : Row := ⟨view.scrollRow.val + visualRow⟩
             if let some currentLineStr := getLineFromBuffer buf rIdx then

  return state

  @[simp] def add (r : Row) (n : Nat) : Row := ⟨r.val + n⟩
  @[simp] def sub (r : Row) (n : Nat) : Row := ⟨r.val - n⟩
  instance : OfNat Row n := ⟨⟨n⟩⟩
  instance : LT Row := ⟨fun a b => a.val < b.val⟩
  instance : LE Row := ⟨fun a b => a.val ≤ b.val⟩
  instance (a b : Row) : Decidable (a < b) := inferInstanceAs (Decidable (a.val < b.val))
  instance (a b : Row) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.val ≤ b.val))
  instance : Min Row := ⟨fun a b => if a.val ≤ b.val then a else b⟩
  instance : Max Row := ⟨fun a b => if a.val ≥ b.val then a else b⟩
  instance : HAdd Row Nat Row := ⟨fun r n => ⟨r.val + n⟩⟩
  instance : HAdd Row Nat Nat := ⟨fun r n => r.val + n⟩
  instance : HSub Row Row Nat := ⟨fun a b => a.val - b.val⟩
  instance : HSub Row Nat Row := ⟨fun r n => ⟨r.val - n⟩⟩
  instance : HSub Row Nat Nat := ⟨fun r n => r.val - n⟩

instance : OfNat Row n := ⟨⟨n⟩⟩
instance : LT Row := ⟨fun a b => a.val < b.val⟩
instance : LE Row := ⟨fun a b => a.val ≤ b.val⟩
instance (a b : Row) : Decidable (a < b) := inferInstanceAs (Decidable (a.val < b.val))
instance (a b : Row) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.val ≤ b.val))
instance : Min Row := ⟨fun a b => if a.val ≤ b.val then a else b⟩
instance : Max Row := ⟨fun a b => if a.val ≥ b.val then a else b⟩
instance : Add Row := ⟨fun a b => ⟨a.val + b.val⟩⟩
instance : Sub Row := ⟨fun a b => ⟨a.val - b.val⟩⟩
instance : HAdd Row Nat Row := ⟨fun r n => ⟨r.val + n⟩⟩
instance : HSub Row Nat Row := ⟨fun r n => ⟨r.val - n⟩⟩
instance : Coe Row Nat := ⟨(·.val)⟩
instance : GetElem (List α) Row α (fun l r => r.val < l.length) where
  getElem l r h := l[r.val]
instance : GetElem (Array α) Row α (fun a r => r.val < a.size) where
  getElem a r h := a[r.val]

  @[simp] def add (c : Col) (n : Nat) : Col := ⟨c.val + n⟩
  @[simp] def sub (c : Col) (n : Nat) : Col := ⟨c.val - n⟩
  instance : OfNat Col n := ⟨⟨n⟩⟩
  instance : LT Col := ⟨fun a b => a.val < b.val⟩
  instance : LE Col := ⟨fun a b => a.val ≤ b.val⟩
  instance (a b : Col) : Decidable (a < b) := inferInstanceAs (Decidable (a.val < b.val))
  instance (a b : Col) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.val ≤ b.val))
  instance : Min Col := ⟨fun a b => if a.val ≤ b.val then a else b⟩
  instance : Max Col := ⟨fun a b => if a.val ≥ b.val then a else b⟩
  instance : HAdd Col Nat Col := ⟨fun c n => ⟨c.val + n⟩⟩
  instance : HAdd Col Nat Nat := ⟨fun c n => c.val + n⟩
  instance : HSub Col Nat Col := ⟨fun c n => ⟨c.val - n⟩⟩
  instance : HSub Col Col Nat := ⟨fun a b => a.val - b.val⟩

instance : OfNat Col n := ⟨⟨n⟩⟩
instance : LT Col := ⟨fun a b => a.val < b.val⟩
instance : LE Col := ⟨fun a b => a.val ≤ b.val⟩
instance (a b : Col) : Decidable (a < b) := inferInstanceAs (Decidable (a.val < b.val))
instance (a b : Col) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.val ≤ b.val))
instance : Min Col := ⟨fun a b => if a.val ≤ b.val then a else b⟩
instance : Max Col := ⟨fun a b => if a.val ≥ b.val then a else b⟩
instance : Add Col := ⟨fun a b => ⟨a.val + b.val⟩⟩
instance : Sub Col := ⟨fun a b => ⟨a.val - b.val⟩⟩
instance : HAdd Col Nat Col := ⟨fun c n => ⟨c.val + n⟩⟩
instance : HSub Col Nat Col := ⟨fun c n => ⟨c.val - n⟩⟩
instance : Coe Col Nat := ⟨(·.val)⟩
instance : GetElem (List α) Col α (fun l c => c.val < l.length) where
  getElem l c h := l[c.val]
instance : GetElem (Array α) Col α (fun a c => c.val < a.size) where
  getElem a c h := a[c.val]

  def make (row col : Nat) : Point := ⟨⟨row⟩, ⟨col⟩⟩

  def make (row : Row) (col : Col) : Point := ⟨row, col⟩
  def fromNat (r c : Nat) : Point := ⟨⟨r⟩, ⟨c⟩⟩

structure RenderCache where
  /-- Visual string for a line, cached to avoid re-calculating widths/tabs/etc. -/
  lineMap : List (Row × String)
  deriving Inhabited
namespace RenderCache
  def find (c : RenderCache) (r : Row) : Option String :=
    c.lineMap.find? (fun (row, _) => row == r) |>.map (fun (_, s) => s)
  def update (c : RenderCache) (r : Row) (s : String) : RenderCache :=
    -- Simple prepend and filter to keep it fresh. In a real editor we might want to cap the size.
    let newMap := (r, s) :: (c.lineMap.filter (fun (row, _) => row != r))
    { lineMap := if newMap.length > 200 then newMap.take 200 else newMap }
end RenderCache

  cache : RenderCache

  cache := { lineMap := [] }

  def clearCache (buf : FileBuffer) : FileBuffer :=
    { buf with cache := { lineMap := [] } }

  clipboard : Option TextBuffer -- Yank buffer

  clipboard : Option String -- Yank buffer (String instead of TextBuffer)

def EditorState.isInSelection (s : EditorState) (row col : Nat) : Bool :=

def EditorState.isInSelection (s : EditorState) (row : Row) (col : Col) : Bool :=

       row >= minRow.val && row <= maxRow.val && col >= minCol.val && col <= maxCol.val

       row >= minRow && row <= maxRow && col >= minCol && col <= maxCol

       if row < p1.row.val || row > p2.row.val then false
       else if row > p1.row.val && row < p2.row.val then true
       else if p1.row.val == p2.row.val then col >= p1.col.val && col <= p2.col.val
       else if row == p1.row.val then col >= p1.col.val
       else if row == p2.row.val then col <= p2.col.val

       if row < p1.row || row > p2.row then false
       else if row > p1.row && row < p2.row then true
       else if p1.row == p2.row then col >= p1.col && col <= p2.col
       else if row == p1.row then col >= p1.col
       else if row == p2.row then col <= p2.col

def EditorState.getSelectedText (s : EditorState) : TextBuffer :=

def EditorState.getSelectedText (s : EditorState) : String :=

  | none => #[]

  | none => ""

    let buffer := s.getActiveBuffer

      let minRow := min startPt.row cursor.row
      let maxRow := max startPt.row cursor.row
      let minCol := min startPt.col cursor.col
      let maxCol := max startPt.col cursor.col
      let content := s.activeBufferContent
      (List.range (maxRow.val - minRow.val + 1)).toArray.map fun i =>
        let row := minRow.val + i
        let line := getLine content row |>.getD ""
        let chars := line.toList
        stringToLine (String.ofList (chars.drop minCol.val |>.take (maxCol.val - minCol.val + 1)))

      let minRow := (min startPt.row cursor.row).val
      let maxRow := (max startPt.row cursor.row).val
      let minCol := (min startPt.col cursor.col).val
      let maxCol := (max startPt.col cursor.col).val
      let lines := (List.range (maxRow - minRow + 1)).map fun i =>
        let r := minRow + i
        let line := ViE.getLineFromBuffer buffer ⟨r⟩ |>.getD ""
        let sub := line.toRawSubstring.drop minCol |>.take (maxCol - minCol + 1)
        sub.toString
      String.intercalate "\n" lines

      let content := s.activeBufferContent
      if p1.row == p2.row then
        let line := getLine content p1.row.val |>.getD ""
        let chars := line.toList
        #[stringToLine (String.ofList (chars.drop p1.col.val |>.take (p2.col.val - p1.col.val + 1)))]
      else
        let firstLine := getLine content p1.row.val |>.getD ""
        let lastLine := getLine content p2.row.val |>.getD ""
        let midLines := arrayDrop (arrayTake content p2.row.val) (p1.row.val + 1)
        let firstPart := stringToLine (String.ofList (firstLine.toList.drop p1.col.val))
        let lastPart := stringToLine (String.ofList (lastLine.toList.take (p2.col.val + 1)))
        arrayConcat [#[firstPart], midLines, #[lastPart]]

      let startOff := buffer.table.getOffsetFromPoint p1.row.val p1.col.val |>.getD 0
      let endOff := buffer.table.getOffsetFromPoint p2.row.val (p2.col.val + 1) |>.getD buffer.table.tree.length
      PieceTable.PieceTree.getSubstring buffer.table.tree startOff (endOff - startOff) buffer.table

  { s.exitVisualMode with clipboard := some text, message := s!"Yanked {text.size} lines" }

  { s.exitVisualMode with clipboard := some text, message := s!"Yanked selection" }

      let minRow := min startPt.row cursor.row
      let maxRow := max startPt.row cursor.row
      let minCol := min startPt.col cursor.col
      let maxCol := max startPt.col cursor.col
      let s' := s.updateActiveBufferContent fun buffer =>
         buffer.mapIdx fun i lineArr =>
           let line := lineToString lineArr
           if i >= minRow.val && i <= maxRow.val then
             let chars := line.toList
             if minCol.val < chars.length then
               let before := chars.take minCol.val
               let after := chars.drop (maxCol.val + 1)
               stringToLine (String.ofList (before ++ after))
             else
               lineArr
           else
             lineArr
      (s'.setCursor (Point.make minRow.val minCol.val)).exitVisualMode

      let minRow := (min startPt.row cursor.row).val
      let maxRow := (max startPt.row cursor.row).val
      let minCol := (min startPt.col cursor.col).val
      let maxCol := (max startPt.col cursor.col).val
      let s' := (List.range (maxRow - minRow + 1)).foldl (init := s) fun st i =>
        let r := minRow + i
        st.updateActiveBuffer fun buffer =>
          match buffer.table.getLineRange r with
          | some (lineStart, lineLen) =>
            let start := lineStart + minCol
            let len := min (maxCol - minCol + 1) (if lineLen > minCol then lineLen - minCol else 0)
            if len > 0 then
              { buffer with table := buffer.table.delete start len start, dirty := true }
            else buffer
          | none => buffer
      s'.exitVisualMode |>.setCursor { row := ⟨minRow⟩, col := ⟨minCol⟩ }

      let s' := s.updateActiveBufferContent fun buffer =>
        if p1.row == p2.row then
          modifyLine buffer p1.row.val fun line =>
            let chars := line.toList
            let before := chars.take p1.col.val
            let after := chars.drop (p2.col.val + 1)
            String.ofList (before ++ after)
        else
          let beforeLines := arrayTake buffer p1.row.val
          let afterLines := arrayDrop buffer (p2.row.val + 1)
          let firstLine := getLine buffer p1.row.val |>.getD ""
          let lastLine := getLine buffer p2.row.val |>.getD ""
          let newJoinedLine := stringToLine (String.ofList (firstLine.toList.take p1.col.val ++ lastLine.toList.drop (p2.col.val + 1)))
          arrayConcat [beforeLines, #[newJoinedLine], afterLines]
      (s'.setCursor p1).exitVisualMode

      let s' := s.updateActiveBuffer fun buffer =>
        let startOff := buffer.table.getOffsetFromPoint p1.row.val p1.col.val |>.getD 0
        let endOff := buffer.table.getOffsetFromPoint p2.row.val (p2.col.val + 1) |>.getD buffer.table.tree.length
        { buffer with table := buffer.table.delete startOff (endOff - startOff) startOff, dirty := true }
      s'.exitVisualMode |>.setCursor p1

  -- let currentLine := getLine s.activeBufferContent cursor.row.val |>.getD ""

     s.setCursor (Point.make cursor.row.val (cursor.col.val - 1))

     s.setCursor { cursor with col := ⟨cursor.col.val - 1⟩ }

  let limit := getLineLengthFromBuffer buffer cursor.row.val |>.getD 0

  let limit := ViE.getLineLengthFromBuffer buffer cursor.row |>.getD 0

     s.setCursor (Point.make cursor.row.val (cursor.col.val + 1))

     s.setCursor { cursor with col := ⟨cursor.col.val + 1⟩ }

    let newRow := cursor.row.val - 1
    let lineLen := getLineLengthFromBuffer s.getActiveBuffer newRow |>.getD 0
    s.setCursor (Point.make newRow (min cursor.col.val lineLen))

    let newRow : Row := ⟨cursor.row.val - 1⟩
    let lineLen := ViE.getLineLengthFromBuffer s.getActiveBuffer newRow |>.getD 0
    s.setCursor { cursor with row := newRow, col := ⟨min cursor.col.val lineLen⟩ }

    let newRow := cursor.row.val + 1
    let lineLen := getLineLengthFromBuffer buffer newRow |>.getD 0
    s.setCursor (Point.make newRow (min cursor.col.val lineLen))

    let newRow : Row := ⟨cursor.row.val + 1⟩
    let lineLen := ViE.getLineLengthFromBuffer buffer newRow |>.getD 0
    s.setCursor { cursor with row := newRow, col := ⟨min cursor.col.val lineLen⟩ }

  let len := getLineLengthFromBuffer s.getActiveBuffer cursor.row.val |>.getD 0
  let newCol := min (col - 1) len -- 1-indexed to 0-indexed, clamped
  let s' := s.setCursor (Point.make cursor.row.val newCol)

  let len := ViE.getLineLengthFromBuffer s.getActiveBuffer cursor.row |>.getD 0
  let newCol : Col := ⟨min (col - 1) len⟩ -- 1-indexed to 0-indexed, clamped
  let s' := s.setCursor { cursor with col := newCol }

  let newRow := if line == 0 then 0 else min (line - 1) (maxLine - 1)
  let lineLen := getLineLengthFromBuffer buffer newRow |>.getD 0

  let newRowVal := if line == 0 then 0 else min (line - 1) (maxLine - 1)
  let newRow : Row := ⟨newRowVal⟩
  let lineLen := ViE.getLineLengthFromBuffer buffer newRow |>.getD 0

  let newCol := min cursor.col.val lineLen
  let s' := s.setCursor (Point.make newRow newCol)

  let newCol : Col := ⟨min cursor.col.val lineLen⟩
  let s' := s.setCursor { cursor with row := newRow, col := newCol }

  let len := getLineLengthFromBuffer s.getActiveBuffer cursor.row.val |>.getD 0
  s.setCursor (Point.make cursor.row.val len)

  let len := ViE.getLineLengthFromBuffer s.getActiveBuffer cursor.row |>.getD 0
  s.setCursor { cursor with col := ⟨len⟩ }

  let cursor := s.getCursor
  let len := ViE.getLineLengthFromBuffer s.getActiveBuffer cursor.row |>.getD 0
  match s.mode with
  | Mode.insert =>
    if cursor.col.val > len then
      s.setCursor { cursor with col := ⟨len⟩ }
    else
      s
  | _ => -- Normal, Visual etc.
    if len == 0 then
      s.setCursor { cursor with col := ⟨0⟩ }
    else if cursor.col.val >= len then
      s.setCursor { cursor with col := ⟨len - 1⟩ }
    else
      s
def isKeyword (c : Char) : Bool :=
  c.isAlphanum || c == '_'
mutual
  partial def findNextForward (buffer : FileBuffer) (row : Row) (col : Col) (started : Bool) : Row × Col :=
    let lineLen := ViE.getLineLengthFromBuffer buffer row |>.getD 0
    if lineLen == 0 then
       (row, 0) -- Stop at empty line
    else if col.val >= lineLen then
       -- End of line, wrap to next line
       if row.val + 1 < FileBuffer.lineCount buffer then
         let nextRow := row.succ
         let nextLen := ViE.getLineLengthFromBuffer buffer nextRow |>.getD 0
         if nextLen == 0 then
            (nextRow, 0) -- Stop at empty line
         else
            findNextForward buffer nextRow 0 true
       else
         (row, col) -- End of file
    else
      let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""
      let c := List.getD lineStr.toList col.val ' '
      let isKw := isKeyword c
      let isSpace := c.isWhitespace
      if !started then
        if isSpace then
           findNextForward buffer row col.succ true
        else
           findNextWordEndForward buffer row col.succ isKw
      else
         if isSpace then
            findNextForward buffer row col.succ started
         else
            (row, col) -- Found start of next word
  partial def findNextWordEndForward (buffer : FileBuffer) (row : Row) (col : Col) (wasTv : Bool) : Row × Col :=
       let lineLen := ViE.getLineLengthFromBuffer buffer row |>.getD 0
       if col.val >= lineLen then
          if row.val + 1 < FileBuffer.lineCount buffer then
            findNextForward buffer row.succ 0 true
          else
            (row, col)
       else
          let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""
          let c := List.getD lineStr.toList col.val ' '
          let isKw := isKeyword c
          let isSpace := c.isWhitespace
          if isSpace then
             findNextForward buffer row col.succ true
          else if isKw != wasTv then
             (row, col)
          else
             findNextWordEndForward buffer row col.succ wasTv
end
/-- Move forward to start of next word (w) -/
def EditorState.moveWordForward (s : EditorState) : EditorState :=
  let buffer := s.getActiveBuffer

  let len := getLineLengthFromBuffer s.getActiveBuffer cursor.row.val |>.getD 0
  if cursor.col.val > len then
    s.setCursor (Point.make cursor.row.val len)

  let currLineLen := ViE.getLineLengthFromBuffer buffer cursor.row |>.getD 0
  let (r, c) := if currLineLen == 0 then
                   if cursor.row.val + 1 < FileBuffer.lineCount buffer then
                      findNextForward buffer cursor.row.succ 0 true
                   else
                      (cursor.row, 0)
                else
                   let lineStr := ViE.getLineFromBuffer buffer cursor.row |>.getD ""
                   if cursor.col.val < currLineLen then
                      let ch := List.getD lineStr.toList cursor.col.val ' '
                      let isKw := isKeyword ch
                      let isSpace := ch.isWhitespace
                      if isSpace then
                         findNextForward buffer cursor.row cursor.col.succ true
                      else
                         findNextWordEndForward buffer cursor.row cursor.col.succ isKw
                   else
                      if cursor.row.val + 1 < FileBuffer.lineCount buffer then
                         findNextForward buffer cursor.row.succ 0 true
                      else
                         (cursor.row, ⟨currLineLen⟩)
  let finalLineLen := ViE.getLineLengthFromBuffer buffer r |>.getD 0
  let finalColVal := if r.val + 1 >= FileBuffer.lineCount buffer && c.val >= finalLineLen && finalLineLen > 0 && s.mode != Mode.insert then
                        finalLineLen - 1
                     else
                        min c.val finalLineLen
  s.setCursor { row := r, col := ⟨finalColVal⟩ }
mutual
    partial def findPrevStart (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=
        let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""
        let c := List.getD lineStr.toList col.val ' '
        if c.isWhitespace then
           if col.val == 0 then
              if row.val > 0 then
                 let prevRow := row.pred
                 let prevLen := ViE.getLineLengthFromBuffer buffer prevRow |>.getD 0
                 if prevLen > 0 then findPrevStart buffer prevRow ⟨prevLen - 1⟩ else (prevRow, 0)
              else (0, 0)
           else
              findPrevStart buffer row col.pred
        else
           let isKw := isKeyword c
           consumeWordBackward buffer row col isKw
    partial def consumeWordBackward (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=
        let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""
        let c := List.getD lineStr.toList col.val ' '
        let isKw := isKeyword c
        if c.isWhitespace || isKw != wantKw then
           (row, col.succ)
        else
           if col.val == 0 then (row, 0)
           else consumeWordBackward buffer row col.pred wantKw
end
/-- Move backward to start of previous word (b) -/
def EditorState.moveWordBackward (s : EditorState) : EditorState :=
  let buffer := s.getActiveBuffer
  let cursor := s.getCursor
  if cursor.row.val == 0 && cursor.col.val == 0 then s

    s

      let lineLen := ViE.getLineLengthFromBuffer buffer cursor.row |>.getD 0
      let startCol : Col := if cursor.col.val >= lineLen then ⟨lineLen⟩ else cursor.col
      let (r, c) :=
         if startCol.val == 0 then
            if cursor.row.val > 0 then
               let prevRow := cursor.row.pred
               let prevLen := ViE.getLineLengthFromBuffer buffer prevRow |>.getD 0
               if prevLen > 0 then
                  findPrevStart buffer prevRow ⟨prevLen - 1⟩
               else
                  (prevRow, 0)
            else (0, 0)
         else
            findPrevStart buffer cursor.row startCol.pred
      s.setCursor { row := r, col := c }
mutual
    partial def findNextEnd (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=
    let lineLen := ViE.getLineLengthFromBuffer buffer row |>.getD 0
    if col.val >= lineLen then
       if row.val + 1 < FileBuffer.lineCount buffer then
         findNextEnd buffer row.succ 0
       else
         (row, col)
    else
       let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""
       let c := List.getD lineStr.toList col.val ' '
       if c.isWhitespace then
          findNextEnd buffer row col.succ
       else
          let isKw := isKeyword c
          consumeWordToEnd buffer row col isKw
     partial def consumeWordToEnd (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=
        let lineLen := ViE.getLineLengthFromBuffer buffer row |>.getD 0
        if col.val + 1 >= lineLen then
           (row, col)
        else
           let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""
           let nextC := List.getD lineStr.toList (col.val + 1) ' '
           let nextKw := isKeyword nextC
           if nextC.isWhitespace || nextKw != wantKw then
              (row, col)
           else
              consumeWordToEnd buffer row col.succ wantKw
end

/-- Move to end of word (e) -/
def EditorState.moveWordEnd (s : EditorState) : EditorState :=
  let buffer := s.getActiveBuffer
  let cursor := s.getCursor
  let currLineLen := ViE.getLineLengthFromBuffer buffer cursor.row |>.getD 0
  let startCol : Col := cursor.col.succ
  let (r, c) :=
      if startCol.val >= currLineLen then
         if cursor.row.val + 1 < FileBuffer.lineCount buffer then
            findNextEnd buffer cursor.row.succ 0
         else
            (cursor.row, ⟨currLineLen⟩)
      else
         findNextEnd buffer cursor.row startCol
  s.setCursor { row := r, col := c }

def EditorState.activeBufferContent (s : EditorState) : TextBuffer :=
  ViE.Buffer.fileBufferToTextBuffer s.getActiveBuffer

      let newBuffers := wg.buffers.map fun b => if b.id == v.bufferId then f b else b

      let newBuffers := wg.buffers.map fun b => if b.id == v.bufferId then FileBuffer.clearCache (f b) else b

def EditorState.updateActiveBufferContent (s : EditorState) (f : TextBuffer → TextBuffer) : EditorState :=
  s.updateActiveBuffer fun b => ViE.Buffer.fileBufferUpdateFromTextBuffer b (f (ViE.Buffer.fileBufferToTextBuffer b))

import ViE.Data.PieceTable

  let row := cursor.row.val
  let col := cursor.col.val

    match buffer.table.getOffsetFromPoint row col with

    match buffer.table.getOffsetFromPoint cursor.row.val cursor.col.val with

  s'.setCursor (Point.make row (col + 1))

  s'.setCursor { cursor with col := ⟨cursor.col.val + 1⟩ }

  let row := cursor.row.val
  let col := cursor.col.val

    match buffer.table.getOffsetFromPoint row col with

    match buffer.table.getOffsetFromPoint cursor.row.val cursor.col.val with

  s'.setCursor (Point.make (row + 1) 0)

  s'.setCursor { row := ⟨cursor.row.val + 1⟩, col := 0 }

  let row := cursor.row.val
  let col := cursor.col.val
  if col > 0 then

  if cursor.col.val > 0 then

       match buffer.table.getOffsetFromPoint row (col - 1) with

       match buffer.table.getOffsetFromPoint cursor.row.val (cursor.col.val - 1) with

    s'.setCursor (Point.make row (col - 1))
  else if row > 0 then

    s'.setCursor { cursor with col := ⟨cursor.col.val - 1⟩ }
  else if cursor.row.val > 0 then

    let prevRow := row - 1

    let prevRow : Row := ⟨cursor.row.val - 1⟩

       match buffer.table.getLineRange prevRow with

       match buffer.table.getLineRange prevRow.val with

          -- Check EOL consistency?
          -- cursor for undo should be at start+len (before newline)

    let newCol := (getLine s.activeBufferContent prevRow).map String.length |>.getD 0
    s'.setCursor (Point.make prevRow newCol)

    let newLen := ViE.getLineLengthFromBuffer s'.getActiveBuffer prevRow |>.getD 0
    s'.setCursor { row := prevRow, col := ⟨newLen⟩ }

def EditorState.deleteCharAfterCursor (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  -- Check if valid char at cursor
  let s' := s.updateActiveBuffer fun buffer =>
    match buffer.table.getOffsetFromPoint cursor.row.val cursor.col.val with
    | some offset =>
        -- Ensure we don't delete newline if at end of line (unless J behavior, but x usually doesn't join lines)
        match buffer.table.getLineRange cursor.row.val with
        | some (_, len) =>
           if cursor.col.val < len then
              { buffer with table := buffer.table.delete offset 1 offset
                            dirty := true }
           else
              buffer
        | none => buffer
     | none => buffer

def deleteLine (buffer : TextBuffer) (row : Nat) : TextBuffer :=
  let before := arrayTake buffer row
  let after := arrayDrop buffer (row + 1)
  if before.isEmpty && after.isEmpty then
    emptyTextBuffer -- Minimum one empty line

  -- Cursor stays at same position unless it was last char
  let newBuffer := s'.getActiveBuffer
  let newLen := ViE.getLineLengthFromBuffer newBuffer cursor.row |>.getD 0
  if newLen > 0 && cursor.col.val >= newLen then
     s'.setCursor { cursor with col := ⟨newLen - 1⟩ }

    before ++ after

     s'

  let row := cursor.row.val

    match buffer.table.getLineRange row with

    match buffer.table.getLineRange cursor.row.val with

       let deleteLen := if row < FileBuffer.lineCount buffer - 1 then len + 1 else len

       let deleteLen := if cursor.row.val < FileBuffer.lineCount buffer - 1 then len + 1 else len

  let newBuffer := s'.activeBufferContent
  let newRow := min row (newBuffer.size.pred)
  let currentLineLen := (getLine newBuffer newRow).map String.length |>.getD 0

  let newBuffer := s'.getActiveBuffer
  let newRowVal := min cursor.row.val (newBuffer.lineCount.pred)
  let newRow : Row := ⟨newRowVal⟩
  let currentLineLen := ViE.getLineLengthFromBuffer newBuffer newRow |>.getD 0

  let s'' := s'.setCursor (Point.make newRow newCol)

  let s'' := s'.setCursor { row := newRow, col := ⟨newCol⟩ }

def EditorState.deleteRange (s : EditorState) (p1 p2 : Point) : EditorState :=
  let s' := s.updateActiveBuffer fun buffer =>
     match buffer.table.getOffsetFromPoint p1.row.val p1.col.val,
           buffer.table.getOffsetFromPoint p2.row.val p2.col.val with
     | some off1, some off2 =>
         let startOff := min off1 off2
         let endOff := max off1 off2
         let len := endOff - startOff
         if len > 0 then
            { buffer with table := buffer.table.delete startOff len startOff
                          dirty := true }
         else buffer
     | _, _ => buffer
  -- Move cursor to start of deleted range
  let newStart := if p1.row < p2.row || (p1.row == p2.row && p1.col < p2.col) then p1 else p2
  let s'' := s'.setCursor newStart
  { s'' with inputState := { s''.inputState with previousKey := none } }
def EditorState.changeWord (s : EditorState) : EditorState :=
  let n := if s.getCount == 0 then 1 else s.getCount
  let start := s.getCursor
  -- Apply 'moveWordEnd' n times (recursive helper)
  let rec applyMotionN (st : EditorState) (count : Nat) : EditorState :=
    match count with
    | 0 => st
    | k + 1 => applyMotionN (st.moveWordEnd) k
  let endState := applyMotionN s n
  let endP := endState.getCursor
  -- Inclusive deletion logic for 'e' motion behavior
  let buffer := s.getActiveBuffer
  let lineLen := ViE.getLineLengthFromBuffer buffer endP.row |>.getD 0
  let targetCol := if endP.col.val + 1 <= lineLen then endP.col.val + 1 else lineLen
  let targetP := { endP with col := ⟨targetCol⟩ }

  (s.deleteRange start targetP).setMode Mode.insert

  let s' := s.updateActiveBufferContent fun buffer =>
    let before := arrayTake buffer (cursor.row.val + 1)
    let after := arrayDrop buffer (cursor.row.val + 1)
    arrayConcat [before, #[#[]], after]
  s'.setCursor (Point.make (cursor.row.val + 1) 0)

  let s' := s.updateActiveBuffer fun buffer =>
    match buffer.table.getLineRange cursor.row.val with
    | some (start, len) =>
       { buffer with table := buffer.table.insert (start + len) "\n" (start + len)
                     dirty := true }
    | none => buffer
  s'.setCursor { row := ⟨cursor.row.val + 1⟩, col := 0 }

  let s' := s.updateActiveBufferContent fun buffer =>
    let before := arrayTake buffer cursor.row.val
    let after := arrayDrop buffer cursor.row.val
    arrayConcat [before, #[#[]], after]
  s'.setCursor (Point.make cursor.row.val 0)

  let s' := s.updateActiveBuffer fun buffer =>
    match buffer.table.getLineRange cursor.row.val with
    | some (start, _) =>
       { buffer with table := buffer.table.insert start "\n" start
                     dirty := true }
    | none => buffer
  s'.setCursor { cursor with col := 0 }

  let line := getLine s.activeBufferContent cursor.row.val |>.getD ""
  { s with clipboard := some #[stringToLine line], message := "Yanked 1 line" }

  let line := ViE.getLineFromBuffer s.getActiveBuffer cursor.row |>.getD ""
  let content := if line.endsWith "\n" then line else line ++ "\n"
  { s with clipboard := (some content : Option String), message := "Yanked 1 line" }

  | some lines =>

  | some text =>

    let row := cursor.row.val
    -- Convert lines to string block (linewise paste)
    let text := String.intercalate "\n" (lines.toList.map fun l => String.ofList l.toList) ++ "\n"

      let offset := match buffer.table.getOffsetFromPoint (row + 1) 0 with
                    | some off => off
                    | none => buffer.table.tree.length

      let (offset, textToInsert) := match buffer.table.getOffsetFromPoint (cursor.row.val + 1) 0 with
                    | some off => (off, text)
                    | none =>
                        let len := buffer.table.tree.length
                        if len > 0 then
                           -- Check if buffer ends with newline to avoid merging
                           -- (Optimization: ideally check last char directly)
                           let s_full := buffer.table.toString
                           if !s_full.endsWith "\n" then
                              (len, "\n" ++ text)
                           else
                              (len, text)
                        else (0, text)

      -- Break undo grouping to ensure separate paste operations are distinct

      { buffer with table := pt.insert offset text offset

      { buffer with table := pt.insert offset textToInsert offset

    s'.setCursor (Point.make (row + 1) 0)

    s'.setCursor { row := ⟨cursor.row.val + 1⟩, col := 0 }

  | some lines =>

  | some text =>

    let row := cursor.row.val
    let text := String.intercalate "\n" (lines.toList.map fun l => String.ofList l.toList) ++ "\n"

      let offset := match buffer.table.getOffsetFromPoint row 0 with

      let offset := match buffer.table.getOffsetFromPoint cursor.row.val 0 with

       { buffer with table := pt.insert offset text offset

       let textStr : String := text
       { buffer with table := pt.insert offset textStr offset

    s'.setCursor (Point.make row 0)

    s'.setCursor { cursor with col := 0 }

  let currentOffset := match buf.table.getOffsetFromPoint s.getCursor.row.val s.getCursor.col.val with

  let cursor := s.getCursor
  let currentOffset := match buf.table.getOffsetFromPoint cursor.row.val cursor.col.val with

      let s'' := s'.setCursor (Point.make r c)

      let s'' := s'.setCursor { row := ⟨r⟩, col := ⟨c⟩ }

  let currentOffset := match buf.table.getOffsetFromPoint s.getCursor.row.val s.getCursor.col.val with

  let cursor := s.getCursor
  let currentOffset := match buf.table.getOffsetFromPoint cursor.row.val cursor.col.val with

      let s'' := s'.setCursor (Point.make r c)

      let s'' := s'.setCursor { row := ⟨r⟩, col := ⟨c⟩ }

def EditorState.commitEdit (s : EditorState) : EditorState :=
  s.updateActiveBuffer fun buffer =>
    { buffer with table := buffer.table.commit }
/-- Vim Operators -/
def EditorState.deleteWord (s : EditorState) : EditorState :=
  let p1 := s.getCursor
  let s' := s.moveWordForward
  let p2 := s'.getCursor
  s.deleteRange p1 p2

  cache := { lineMap := [] }

  normal := fun s k => match k with

  normal := fun s k =>
  let handleMotion (state : EditorState) (motion : EditorState → EditorState) : IO EditorState :=
      let n := if state.getCount == 0 then 1 else state.getCount
      let rec applyN (st : EditorState) (count : Nat) : EditorState :=
        match count with
        | 0 => st
        | n + 1 => applyN (motion st) n
      termination_by count
      match state.inputState.previousKey with
      | none => pure $ clearInput (EditorState.clampCursor (applyN state n))
      | some 'd' =>
          let start := state.getCursor
          let endP := (applyN state n).getCursor
          pure $ clearInput (state.deleteRange start endP)
      | some 'c' =>
          let start := state.getCursor
          let endP := (applyN state n).getCursor
          pure $ clearInput (state.deleteRange start endP |>.setMode Mode.insert)
      | _ => pure $ clearInput (EditorState.clampCursor (applyN state n))
  match k with

        pure $ clearInput (EditorState.moveCursorLeftN s s.getCount)
  | Key.char 'j' => pure $ clearInput (EditorState.moveCursorDownN s s.getCount)
  | Key.char 'k' => pure $ clearInput (EditorState.moveCursorUpN s s.getCount)
  | Key.char 'l' => pure $ clearInput (EditorState.moveCursorRightN s s.getCount)

        handleMotion s EditorState.moveCursorLeft
  | Key.char 'j' => handleMotion s EditorState.moveCursorDown
  | Key.char 'k' => handleMotion s EditorState.moveCursorUp
  | Key.char 'l' => handleMotion s EditorState.moveCursorRight

     if s.inputState.countBuffer.isEmpty then pure $ clearInput (EditorState.moveToLineStart s)

     if s.inputState.countBuffer.isEmpty then handleMotion s EditorState.moveToLineStart

  | Key.char '$' => pure $ clearInput (EditorState.moveToLineEnd s)

  | Key.char '$' => handleMotion s EditorState.moveToLineEnd
  | Key.char 'w' =>
      match s.inputState.previousKey with
      | some 'c' => pure $ clearInput (s.changeWord)
      | _ => handleMotion s EditorState.moveWordForward
  | Key.char 'b' => handleMotion s EditorState.moveWordBackward
  | Key.char 'e' => handleMotion s EditorState.moveWordEnd
  | Key.char 'x' => pure $ clearInput (EditorState.deleteCharAfterCursor s)

  | Key.char 'c' =>
    match s.inputState.previousKey with
    | some 'c' =>
        -- cc: delete line and enter insert mode
        -- For now, approximate with delete line. Ideally should preserve line as empty.
        pure $ (s.deleteCurrentLine).setMode Mode.insert
    | _ => pure { s with inputState := { s.inputState with previousKey := some 'c' } }

         | 'g' =>
            -- gg implementation
            let n := s.getCount
            let line := if n > 0 then n else 1
            pure $ clearInput (EditorState.jumpToLine s line)

            match s.inputState.previousKey with
            | some 'g' =>
               -- gg implementation
               let n := s.getCount
               let line := if n > 0 then n else 1
               pure $ clearInput (EditorState.jumpToLine s line)
            | _ => pure { s with inputState := { s.inputState with previousKey := some 'g' } }

             pure { s with inputState := { s.inputState with previousKey := some 'g' } }

    | Key.esc => pure $ s.setMode Mode.normal

    | Key.esc => pure $ (s.commitEdit.moveCursorLeft).setMode Mode.normal

    | Key.char 'w' => pure $ clearInput (EditorState.moveWordForward s)
    | Key.char 'b' => pure $ clearInput (EditorState.moveWordBackward s)
    | Key.char 'e' => pure $ clearInput (EditorState.moveWordEnd s)

       -- This case is only reached if we pushed a char and pending became exactly "\x1b",
       -- which is impossible if start condition was "pending.length > 0" (meaning pending was already "\x1b")
       -- UNLESS previous pending was empty? No, then it goes to else block.
       -- Wait, if pending was "\x1b" and we pushed nothing? No, we always push c.
       -- So this case is indeed impossible for Escape+Char.

    if cursor.row < 2 then return state -- Header rows

    if selectedIdx < 0 || selectedIdx >= explorer.entries.length then

    if selectedIdx.val >= explorer.entries.length then

    let entry := explorer.entries[selectedIdx]!

    let entry := explorer.entries[selectedIdx.val]!

          cache := { lineMap := [] }

          cache := { lineMap := [] }

        cache := { lineMap := [] }

      cache := { lineMap := [] }

def getLineFromBuffer (buffer : FileBuffer) (n : Nat) : Option String :=
  buffer.table.getLine n

def getLineFromBuffer (buffer : FileBuffer) (n : Row) : Option String :=
  buffer.table.getLine n.val

def getLineLengthFromBuffer (buffer : FileBuffer) (n : Nat) : Option Nat :=
  buffer.table.getLineLength n

def getLineLengthFromBuffer (buffer : FileBuffer) (n : Row) : Option Nat :=
  buffer.table.getLineLength n.val

      match getLineFromBuffer buf i with

      match getLineFromBuffer buf ⟨i⟩ with

    cache := { lineMap := [] }

def modifyLineInBuffer (buffer : FileBuffer) (row : Nat) (f : String → String) : FileBuffer :=
  match buffer.table.getLineRange row with

def modifyLineInBuffer (buffer : FileBuffer) (row : Row) (f : String → String) : FileBuffer :=
  match buffer.table.getLineRange row.val with

     match buffer.table.getLine row with

     match buffer.table.getLine row.val with

def getLine (buffer : TextBuffer) (n : Nat) : Option String :=
  if h : n < buffer.size then
    some (lineToString buffer[n])

def getLine (buffer : TextBuffer) (n : Row) : Option String :=
  if h : n.val < buffer.size then
    some (lineToString buffer[n.val])

def modifyLine (buffer : TextBuffer) (row : Nat) (f : String → String) : TextBuffer :=
  if h : row < buffer.size then
    let oldLine := buffer[row]

def modifyLine (buffer : TextBuffer) (row : Row) (f : String → String) : TextBuffer :=
  if h : row.val < buffer.size then
    let oldLine := buffer[row.val]

    buffer.set! row newLine

    buffer.set! row.val newLine

def setLine (buffer : TextBuffer) (row : Nat) (content : String) : TextBuffer :=
  buffer.set! row (stringToLine content)

def setLine (buffer : TextBuffer) (row : Row) (content : String) : TextBuffer :=
  buffer.set! row.val (stringToLine content)

  if state.dirty then

  let state ← if state.dirty then

  else
    pure state

        cache := { lineMap := [] }

import Test.Keybinds
import Test.Mode
import Test.BugReproduction

  Test.Keybinds.test
  Test.Mode.test
  Test.BugReproduction.test

import ViE.State.Config
import ViE.Config
import ViE.Command.Impl
import ViE.Key.Map
import ViE.State.Edit
import ViE.State.Movement
namespace Test.Mode
open ViE
def assert (msg : String) (cond : Bool) : IO Unit := do
  if cond then
    IO.println s!"[PASS] {msg}"
  else
    IO.println s!"[FAIL] {msg}"
    throw (IO.userError s!"Assertion failed: {msg}")
-- Helper to construct a full Config
def makeTestConfig : Config := {
  settings := ViE.defaultConfig
  commands := ViE.Command.defaultCommandMap
  bindings := ViE.Key.makeKeyMap ViE.Command.defaultCommandMap
}
-- Run a sequence of keys
def runKeys (startState : EditorState) (keys : List Key) : IO EditorState := do
  let config := makeTestConfig
  let mut s := startState
  for k in keys do
    s ← ViE.update config s k
  return s
def test : IO Unit := do
  IO.println "Starting Mode Test..."
  let s := ViE.initialState
  -- Scenario: Insert 'abc' then Esc.
  -- Initial: (0,0)
  -- 'i' -> Insert Mode
  -- 'a' -> "a", (0,1)
  -- 'b' -> "ab", (0,2)
  -- 'c' -> "abc", (0,3)
  -- Esc -> Normal Mode.
  -- Expected Vim behavior: Cursor should move left to (0,2) 'c'.
  -- If empty line "insert a then esc", "a" (0,1) -> (0,0).
  let keys := [Key.char 'i', Key.char 'a', Key.char 'b', Key.char 'c', Key.esc]
  let sEnd ← runKeys s keys
  -- Check Mode
  if sEnd.mode != Mode.normal then
    IO.println s!"[FAIL] Mode mismatch. Expected Normal, got {sEnd.mode}"
    assert "Mode is Normal" false
  else
    IO.println "[PASS] Mode is Normal"
  -- Check Text
  let text := getLineFromBuffer sEnd.getActiveBuffer 0 |>.getD ""
  if text != "abc" then
    IO.println s!"[FAIL] Text mismatch. Expected 'abc', got '{text}'"
    assert "Text is 'abc'" false
  else
     IO.println "[PASS] Text is 'abc'"
  -- Check Cursor
  -- Expect (0, 2)
  let cursor := sEnd.getCursor
  if cursor.col.val != 2 then
    IO.println s!"[FAIL] Cursor mismatch. Expected (0, 2), got ({cursor.row.val}, {cursor.col.val})"
    assert "Cursor moved left on Esc" false
  else
    IO.println "[PASS] Cursor moved left on Esc"
  IO.println "ModeTest passed!"
end Test.Mode

import ViE.State.Movement
import ViE.State.Edit
import ViE.Key.Map
import ViE.Types
import ViE.Buffer.Content
import ViE.Config
import ViE.Command.Impl
namespace Test.Keybinds
open ViE
def makeTestConfig : Config := {
  settings := ViE.defaultConfig
  commands := ViE.Command.defaultCommandMap
  bindings := ViE.Key.makeKeyMap ViE.Command.defaultCommandMap
}
def keys (s : String) : List Key :=
  s.toList.map fun c =>
    if c == '\n' then Key.enter else Key.char c
def runKeys (s : EditorState) (ks : List Key) : IO EditorState := do
  let config := makeTestConfig
  ks.foldlM (fun s k => ViE.update config s k) s
def assert (msg : String) (cond : Bool) : IO Unit := do
  if !cond then
    throw (IO.userError s!"Assertion failed: {msg}")
def testMotions : IO Unit := do
  IO.println "  Testing Motions..."
  let s0 := ViE.initialState
  let s1 ← runKeys s0 ([Key.char 'i'] ++ keys "line1\nline2\nline3" ++ [Key.esc] ++ keys "gg0")
  -- "line1\nline2\nline3" cursor at (0,0)
  -- l, h
  let s_l ← runKeys s1 [Key.char 'l']
  if s_l.getCursor != Point.make 0 1 then
     let c := s_l.getCursor
     let line := ViE.getLineFromBuffer s_l.getActiveBuffer c.row |>.getD "ERR"
     let len := ViE.getLineLengthFromBuffer s_l.getActiveBuffer c.row |>.getD 999
     IO.println s!"DEBUG FAILURE: l motion. Cursor: ({c.row.val}, {c.col.val}). Line 0: '{line}' (len: {len})"
  assert "l moves right" (s_l.getCursor == Point.make 0 1)
  let s_lh ← runKeys s_l [Key.char 'h']
  assert "h moves left" (s_lh.getCursor == Point.make 0 0)
  -- j, k
  let s_j ← runKeys s1 [Key.char 'j']
  assert "j moves down" (s_j.getCursor == Point.make 1 0)
  let s_jk ← runKeys s_j [Key.char 'k']
  assert "k moves up" (s_jk.getCursor == Point.make 0 0)
  -- 0, $
  -- 0, $
  let s_end ← runKeys s1 [Key.char '$']
  assert "$ moves to end" (s_end.getCursor == Point.make 0 4) -- '1' is at col 4
  let s_start ← runKeys s_end [Key.char '0']
  assert "0 moves to start" (s_start.getCursor == Point.make 0 0)
  -- w, b, e
  let s_text ← runKeys s0 ([Key.char 'i'] ++ keys "word1 word2" ++ [Key.esc] ++ [Key.char '0'])
  let s_w ← runKeys s_text [Key.char 'w']
  assert "w moves to next word" (s_w.getCursor == Point.make 0 6)
  let s_e ← runKeys s_text [Key.char 'e']
  assert "e moves to end of word" (s_e.getCursor == Point.make 0 4)
  let s_we ← runKeys s_w [Key.char 'e']
  assert "we moves to end of next word" (s_we.getCursor == Point.make 0 10)
  let s_web ← runKeys s_we [Key.char 'b']
  assert "b moves to start of word" (s_web.getCursor == Point.make 0 6)
  -- gg, G
  let s_G ← runKeys s1 [Key.char 'G']
  assert "G moves to last line" (s_G.getCursor.row == 2)
  let s_gg ← runKeys s_G [Key.char 'g', Key.char 'g']
  assert "gg moves to first line" (s_gg.getCursor.row == 0)
  -- | (jump to column)
  let s_pipe ← runKeys s1 [Key.char '3', Key.char '|']
  assert "| jumps to column" (s_pipe.getCursor.col == 2) -- 1-indexed count 3 -> col 2
def testEditing : IO Unit := do
  IO.println "  Testing Editing..."
  let s0 := ViE.initialState
  -- i, a, A
  let s_i ← runKeys s0 [Key.char 'i', Key.char 'x', Key.esc]
  assert "i inserts" (s_i.getActiveBuffer.table.toString == "x")
  let s_a ← runKeys s_i [Key.char 'a', Key.char 'y', Key.esc]
  assert "a appends" (s_a.getActiveBuffer.table.toString == "xy")
  let s_A ← runKeys s_a [Key.char '0', Key.char 'A', Key.char 'z', Key.esc]
  assert "A appends at end" (s_A.getActiveBuffer.table.toString == "xyz")
  -- o, O
  let s_o ← runKeys s_i [Key.char 'o', Key.char 'y', Key.esc]
  assert "o inserts line below" (s_o.getActiveBuffer.table.toString == "x\ny")
  let s_O ← runKeys s_o [Key.char 'k', Key.char 'O', Key.char 'z', Key.esc]
  assert "O inserts line above" (s_O.getActiveBuffer.table.toString == "z\nx\ny")
  -- x
  let s_x ← runKeys s_i [Key.char 'x']
  assert "x deletes char" (s_x.getActiveBuffer.table.toString == "")
def testOperators : IO Unit := do
  IO.println "  Testing Operators..."
  let s0 := ViE.initialState
  let s1 ← runKeys s0 ([Key.char 'i'] ++ keys "hello world" ++ [Key.esc] ++ [Key.char '0'])
  -- dw
  let s_dw ← runKeys s1 [Key.char 'd', Key.char 'w']
  assert "dw deletes word" (s_dw.getActiveBuffer.table.toString == "world")
  -- cw
  let s_cw ← runKeys s1 [Key.char 'c', Key.char 'w', Key.char 'h', Key.char 'i', Key.esc]
  assert "cw changes word" (s_cw.getActiveBuffer.table.toString == "hi world")
  -- dd
  let s_lines ← runKeys s0 ([Key.char 'i'] ++ keys "line1\nline2\nline3" ++ [Key.esc] ++ keys "ggj")
  let s_dd ← runKeys s_lines [Key.char 'd', Key.char 'd']
  assert "dd deletes current line" (s_dd.getActiveBuffer.table.toString == "line1\nline3")
  -- yy, p, P
  let s_yy ← runKeys s_lines [Key.char 'g', Key.char 'g', Key.char 'y', Key.char 'y']
  let s_p ← runKeys s_yy [Key.char 'G', Key.char 'p']
  let p_res := s_p.getActiveBuffer.table.toString
  if p_res != "line1\nline2\nline3\nline1\n" then
     IO.println s!"DEBUG FAILURE: p paste. Expected 'line1\\nline2\\nline3\\nline1\\n', got '{p_res}'"
  assert "p pastes below" (s_p.getActiveBuffer.table.toString == "line1\nline2\nline3\nline1\n")
  let s_P ← runKeys s_yy [Key.char 'g', Key.char 'g', Key.char 'P']
  assert "P pastes above" (s_P.getActiveBuffer.table.toString == "line1\nline1\nline2\nline3")
def testVisual : IO Unit := do
  IO.println "  Testing Visual Mode..."
  let s0 := ViE.initialState
  let s1 ← runKeys s0 ([Key.char 'i'] ++ keys "highlight me" ++ [Key.esc] ++ [Key.char '0'])
  -- v, d
  let s_v ← runKeys s1 [Key.char 'v', Key.char 'l', Key.char 'd']
  assert "visual d deletes selection" (s_v.getActiveBuffer.table.toString == "ghlight me")
  -- v, y, p
  let s_vy ← runKeys s1 [Key.char 'v', Key.char 'e', Key.char 'y']
  let s_vyp ← runKeys s_vy [Key.char '$', Key.char 'p']
  assert "visual y yanks selection" (s_vyp.getActiveBuffer.table.toString == "highlight me\nhighlight")
def testCounted : IO Unit := do
  IO.println "  Testing Counted Actions..."
  let s0 := ViE.initialState
  let s1 ← runKeys s0 ([Key.char 'i'] ++ keys "a b c d e" ++ [Key.esc] ++ [Key.char '0'])
  -- 3w
  let s_3w ← runKeys s1 [Key.char '3', Key.char 'w']
  assert "3w moves 3 words" (s_3w.getCursor.col == 6) -- positions of 'a', 'b', 'c', 'd' start: 0, 2, 4, 6
  -- 2dd
  let s_lines ← runKeys s0 ([Key.char 'i'] ++ keys "1\n2\n3\n4" ++ [Key.esc] ++ [Key.char 'g', Key.char 'g'])
  -- Not all counted actions might be implemented yet, check Map.lean
  -- Map.lean uses s.getCount for h,j,k,l. dd uses previousKey, doesn't seem to use count yet.
  -- Let's test what is implemented.
  -- 2j
  let s_2j ← runKeys s_lines [Key.char '2', Key.char 'j']
  assert "2j moves 2 lines down" (s_2j.getCursor.row == 2)
def test : IO Unit := do
  IO.println "Starting Expanded Keybind Tests..."
  testMotions
  testEditing
  testOperators
  testVisual
  testCounted
  IO.println "All Expanded Keybind Tests passed!"
end Test.Keybinds

  assert s!"Cursor after insert 'd' should be (0,1) but is ({c3.row.val}, {c3.col.val})" (c3.row.val == 0 && c3.col.val == 1)

  assert s!"Cursor after insert 'd' and Esc should be (0,0) but is ({c3.row.val}, {c3.col.val})" (c3.row.val == 0 && c3.col.val == 0)

import ViE.State.Config
import ViE.Config
import ViE.Command.Impl
import ViE.Key.Map
import ViE.State.Edit
namespace Test.BugReproduction
open ViE
def assert (msg : String) (cond : Bool) : IO Unit := do
  if cond then
    IO.println s!"[PASS] {msg}"
  else
    IO.println s!"[FAIL] {msg}"
    throw (IO.userError s!"Assertion failed: {msg}")
-- Helper to construct a full Config
def makeTestConfig : Config := {
  settings := ViE.defaultConfig
  commands := ViE.Command.defaultCommandMap
  bindings := ViE.Key.makeKeyMap ViE.Command.defaultCommandMap
}
-- Run a sequence of keys
def runKeys (startState : EditorState) (keys : List Key) : IO EditorState := do
  let config := makeTestConfig
  let mut s := startState
  for k in keys do
    s ← ViE.update config s k
  return s
def test : IO Unit := do
  IO.println "Starting Bug Reproduction Test..."
  let s := ViE.initialState
  -- Scenario: Insert, Undo, Insert
  let s1 := s.insertChar 'a'
  let s1 := s1.commitEdit -- Force separate undo group
  let s2 := s1.insertChar 'b'
  -- Text: 'ab', Cursor: (0, 2)
  let s3 := s2.undo
  -- Text: 'a', Cursor should be (0, 1)
  let cursor := s3.getCursor
  if cursor.col.val != 1 then
     IO.println s!"[FAIL] Undo cursor mismatch. Expected 1, got {cursor.col.val}"
     assert "Undo cursor" false
  else
     IO.println "[PASS] Undo cursor correct"
  let s4 := s3.insertChar 'c'
  -- Text: 'ac'
  let text := getLineFromBuffer s4.getActiveBuffer 0 |>.getD ""
  if text != "ac" then
      IO.println s!"[FAIL] Insert after undo failed. Expected 'ac', got '{text}'"
      assert "Insert after undo" false
  else
      IO.println "[PASS] Insert after undo works"
  -- Scenario: Paste, Undo, Paste (checking grouping too, but focusing on cursor)
  -- Reset
  let s := ViE.initialState
  let 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 command
  let s := ViE.initialState
  let 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 setCursor
  let 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" then
     IO.println s!"[FAIL] 'x' command (deleteCharAfterCursor) failed. Expected 'hy', got '{text}'"
     assert "x command" false
  else
     IO.println "[PASS] 'x' command works"
  IO.println "Bug Reproduction Test Finished"
end Test.BugReproduction

- `w`: Move forward to start of next word
- `b`: Move backward to start of previous word
- `e`: Move forward to end of word

- `cw`: Change word
- `x`: Delete character

- `P`: paste yanked line above

- `w/b/e`: extend selection by word
- `d/x`: delete selection
- `y`: yank selection