testDriver = "test"

  let mut buffer := ""

  let mut buffer : Array String := #[]

  buffer := buffer ++ Terminal.hideCursorStr ++ Terminal.homeCursorStr

  buffer := buffer.push Terminal.hideCursorStr
  buffer := buffer.push Terminal.homeCursorStr

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

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

      let mut winBuf := ""

      let mut winBuf : Array String := #[]

        winBuf := winBuf ++ Terminal.moveCursorStr screenRow c

        winBuf := winBuf.push (Terminal.moveCursorStr screenRow c)

             winBuf := winBuf ++ s!"{leftPad (toString (lineIdx.val + 1)) 3} "

             winBuf := winBuf.push s!"{leftPad (toString (lineIdx.val + 1)) 3} "

           | none => winBuf := winBuf ++ displayLine

           | none => winBuf := winBuf.push displayLine

                  winBuf := winBuf ++ "\x1b[7m" -- Inverse video

                  winBuf := winBuf.push "\x1b[7m" -- Inverse video

                  winBuf := winBuf ++ "\x1b[0m"

                  winBuf := winBuf.push "\x1b[0m"

                winBuf := winBuf ++ ch.toString

                winBuf := winBuf.push ch.toString

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

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

           winBuf := winBuf ++ st.config.emptyLineMarker

           winBuf := winBuf.push st.config.emptyLineMarker

        winBuf := winBuf ++ Terminal.clearLineStr

        winBuf := winBuf.push Terminal.clearLineStr

      winBuf := winBuf ++ Terminal.moveCursorStr statusRow c

      winBuf := winBuf.push (Terminal.moveCursorStr statusRow c)

      winBuf := winBuf ++ st.config.statusBarStyle ++ statusStr.trimAscii ++ Terminal.clearLineStr ++ st.config.resetStyle

      winBuf := winBuf.push st.config.statusBarStyle
      winBuf := winBuf.push statusStr.trimAscii.toString
      winBuf := winBuf.push Terminal.clearLineStr
      winBuf := winBuf.push st.config.resetStyle

      let mut sepStr := ""

      let mut sepStr : Array String := #[]

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

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

      let mut sepStr := ""

      let mut sepStr : Array String := #[]

        sepStr := sepStr ++ Terminal.moveCursorStr sepRow c

        sepStr := sepStr.push (Terminal.moveCursorStr sepRow c)

           sepStr := sepStr ++ st.config.hSplitStr

           sepStr := sepStr.push st.config.hSplitStr

  buffer := buffer ++ Terminal.moveCursorStr (rows - 1) 0

  buffer := buffer.push (Terminal.moveCursorStr (rows - 1) 0)

  buffer := buffer ++ statusRight ++ Terminal.clearLineStr

  buffer := buffer.push statusRight
  buffer := buffer.push Terminal.clearLineStr

  buffer := buffer ++

  buffer := buffer.push (

  )

     buffer := buffer ++ Terminal.moveCursorStr (rows - 1) (1 + state.inputState.commandBuffer.length)

     buffer := buffer.push (Terminal.moveCursorStr (rows - 1) (1 + state.inputState.commandBuffer.length))

    buffer := buffer ++ Terminal.hideCursorStr

    buffer := buffer.push Terminal.hideCursorStr

    buffer := buffer ++ Terminal.showCursorStr

    buffer := buffer.push Terminal.showCursorStr

  IO.print buffer

  let finalStr := String.intercalate "" buffer.toList
  IO.print finalStr

import Lean

open ViE.PieceTable

/-- Editor Mode -/

  deriving Repr, BEq, Ord

  deriving Repr, BEq, Ord, Hashable

  lineMap : List (Row × String)

  lineMap : Lean.RBMap Row String compare

    c.lineMap.find? (fun (row, _) => row == r) |>.map (fun (_, s) => s)

    c.lineMap.find? r

    -- 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 }

    { lineMap := c.lineMap.insert r s }

  cache := { lineMap := [] }

  cache := { lineMap := Lean.RBMap.empty }

    { buf with cache := { lineMap := [] } }

    { buf with cache := { lineMap := Lean.RBMap.empty } }

      PieceTable.PieceTree.getSubstring buffer.table.tree startOff (endOff - startOff) buffer.table

      PieceTree.getSubstring buffer.table.tree startOff (endOff - startOff) buffer.table

                           let s_full := buffer.table.toString
                           if !s_full.endsWith "\n" then
                              (len, "\n" ++ text)

                           if !PieceTable.endsWithNewline buffer.table then
                               (len, "\n" ++ text)

                              (len, text)

                               (len, text)

import Lean

open ViE.PieceTable

  cache := { lineMap := [] }

  cache := { lineMap := Lean.RBMap.empty }

open ViE.PieceTable

namespace ViE.PieceTable

namespace ViE

/-- Insert text at offset -/

/--
  Insert text at the specified offset.
  params:
  - offset: The byte offset where insertion begins.
  - text: The string content to insert.
  - cursorOffset: The cursor position *after* this insertion, stored in the undo stack
    to restore cursor position when undoing this operation.
-/

/-- Delete range [offset, offset + length) -/

/--
  Delete a range of text.
  params:
  - offset: The starting byte offset of the range to delete.
  - length: The number of bytes to delete.
  - cursorOffset: The cursor position *after* this deletion, stored in the undo stack
    to restore cursor position when undoing this operation.
-/

def PieceTable.length (pt : PieceTable) : Nat := pt.tree.length
/-- Check if the piece table buffer ends with a newline character.
    Optimized to avoid converting the entire buffer to string. -/
def PieceTable.endsWithNewline (pt : PieceTable) : Bool :=
  let len := pt.length
  if len == 0 then false
  else
    let s := PieceTree.getSubstring pt.tree (len - 1) len pt
    s == "\n"

end ViE.PieceTable

end ViE

namespace ViE.PieceTable

namespace ViE

inductive PieceTree where

inductive PieceTree : Type _ where

end ViE.PieceTable

end ViE

namespace ViE.PieceTable

namespace ViE

end ViE.PieceTable

end ViE

namespace ViE.PieceTable

namespace ViE

end ViE.PieceTable

end ViE

import Lean

open ViE.PieceTable

          cache := { lineMap := [] }

          cache := { lineMap := Lean.RBMap.empty }

          cache := { lineMap := [] }

          cache := { lineMap := Lean.RBMap.empty }

        cache := { lineMap := [] }

        cache := { lineMap := Lean.RBMap.empty }

      cache := { lineMap := [] }

      cache := { lineMap := Lean.RBMap.empty }

import Lean

open ViE.PieceTable

    cache := { lineMap := [] }

    cache := { lineMap := Lean.RBMap.empty }

import Lean

open ViE.PieceTable

        cache := { lineMap := [] }

        cache := { lineMap := Lean.RBMap.empty }

import Test.PieceTable.Basic
import Test.PieceTable.UndoRedo
import Test.PieceTable.Appended
import Test.PieceTable.Stress

def main : IO Unit := do

def test : IO Unit := do

  Test.PieceTable.Basic.test
  Test.PieceTable.UndoRedo.test
  Test.PieceTable.Appended.test
  Test.PieceTable.Stress.test

def main : IO Unit := do
  test

import ViE.Types
import ViE.Buffer.Content
import ViE.State.Layout
import ViE.State.Movement
namespace Test.Utils
/-- Assert condition is true, throw error if false -/
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}")
/-- Assert equality with debug output -/
def assertEqual [Repr α] [BEq α] (msg : String) (expected actual : α) : IO Unit := do
  if expected == actual then
    IO.println s!"[PASS] {msg}"
  else
    IO.println s!"[FAIL] {msg}"
    IO.println s!"  Expected: {repr expected}"
    IO.println s!"  Actual:   {repr actual}"
    throw (IO.userError s!"Assertion failed: {msg}")
/-- Assert EditorState buffer content matches expected string -/
def assertBuffer (msg : String) (est : ViE.EditorState) (expected : String) : IO Unit := do
  let actual := est.getActiveBuffer.table.toString
  if actual == expected then
    IO.println s!"[PASS] {msg}"
  else
    IO.println s!"[FAIL] {msg}"
    IO.println s!"  Expected: '{expected}'"
    IO.println s!"  Actual:   '{actual}'"
    throw (IO.userError s!"Buffer content assertion failed: {msg}")
/-- Assert EditorState cursor position matches expected row/col -/
def assertCursor (msg : String) (est : ViE.EditorState) (r c : Nat) : IO Unit := do
  let cursor := est.getCursor
  if cursor.row.val == r && cursor.col.val == c then
    IO.println s!"[PASS] {msg}"
  else
    IO.println s!"[FAIL] {msg}"
    IO.println s!"  Expected: ({r}, {c})"
    IO.println s!"  Actual:   ({cursor.row.val}, {cursor.col.val})"
    throw (IO.userError s!"Cursor assertion failed: {msg}")
end Test.Utils

open ViE.PieceTable

open ViE

import ViE.Data.PieceTable
import Test.Utils
open ViE
namespace Test.PieceTable.UndoRedo
open Test.Utils
def testUndoRedo : IO Unit := do
  IO.println "testUndoRedo..."
  let pt := PieceTable.fromString ""
  -- Insert "A" at 0
  let pt1 := pt.insert 0 "A" 0
  -- Insert "B" at 0 (Prepend) -> "BA"
  let pt2 := pt1.insert 0 "B" 0
  assertEqual "Initial state" "BA" pt2.toString
  -- Undo B (restores to "A")
  let (pt3, _) := pt2.undo 0
  assertEqual "After Undo 1" "A" pt3.toString
  -- Undo A
  let (pt4, _) := pt3.undo 0
  assertEqual "After Undo 2" "" pt4.toString
  -- Redo A
  let (pt5, _) := pt4.redo 0
  assertEqual "After Redo 1" "A" pt5.toString
  -- Redo B
  let (pt6, _) := pt5.redo 0
  assertEqual "After Redo 2" "BA" pt6.toString
def testComplexUndo : IO Unit := do
  IO.println "testComplexUndo..."
  let pt := PieceTable.fromString "Base"
  let pt1 := pt.insert 4 "1" 4 -- Base1
  let pt1 := pt1.commit -- Prevent merge
  let pt2 := pt1.insert 5 "2" 5 -- Base12
  let pt3 := pt2.delete 5 1 5 -- Base1
  let pt4 := pt3.insert 5 "3" 5 -- Base13
  assertEqual "State before undo" "Base13" pt4.toString
  -- Undo insert "3" -> Base1
  let (u1, _) := pt4.undo 0
  assertEqual "Undo 3" "Base1" u1.toString
  -- Undo delete "2" -> Base12
  let (u2, _) := u1.undo 0
  assertEqual "Undo delete 2" "Base12" u2.toString
  -- Undo insert "2" -> Base1
  let (u3, _) := u2.undo 0
  assertEqual "Undo insert 2" "Base1" u3.toString
  -- Undo insert "1" -> Base
  let (u4, _) := u3.undo 0
  assertEqual "Undo insert 1" "Base" u4.toString
def test : IO Unit := do
  IO.println "Starting PieceTable Undo/Redo Test..."
  testUndoRedo
  testComplexUndo
  IO.println "PieceTable Undo/Redo Test passed!"
end Test.PieceTable.UndoRedo

import ViE.Data.PieceTable
import Test.Utils
open ViE
namespace Test.PieceTable.Stress
open Test.Utils
/-- Naive string manipulation for verification -/
def naiveInsert (s : String) (idx : Nat) (content : String) : String :=
  let lst := s.toList
  let pre := lst.take idx
  let post := lst.drop idx
  String.ofList (pre ++ content.toList ++ post)
def naiveDelete (s : String) (idx : Nat) (len : Nat) : String :=
  let lst := s.toList
  let pre := lst.take idx
  let post := lst.drop (idx + len)
  String.ofList (pre ++ post)
def testConsistency : IO Unit := do
  IO.println "testConsistency (Small Stress)..."
  let mut pt := PieceTable.fromString ""
  let mut mirror := ""
  -- 1. Insert Hello
  pt := pt.insert 0 "Hello" 0
  mirror := naiveInsert mirror 0 "Hello"
  assertEqual "Step 1" mirror pt.toString
  -- 2. Insert World
  pt := pt.insert 5 " World" 5
  mirror := naiveInsert mirror 5 " World"
  assertEqual "Step 2" mirror pt.toString
  -- 3. Delete space at 5
  -- "Hello World" -> "HelloWorld"
  pt := pt.delete 5 1 5
  mirror := naiveDelete mirror 5 1
  assertEqual "Step 3" mirror pt.toString
  -- 4. Insert comma at 5
  -- "HelloWorld" -> "Hello,World"
  pt := pt.insert 5 "," 5
  mirror := naiveInsert mirror 5 ","
  assertEqual "Step 4" mirror pt.toString
def test : IO Unit := do
  IO.println "Starting PieceTable Stress Test..."
  testConsistency
  IO.println "PieceTable Stress Test passed!"
end Test.PieceTable.Stress

import ViE.Data.PieceTable
import Test.Utils
open ViE
namespace Test.PieceTable.Basic
open Test.Utils
def testInsert : IO Unit := do
  IO.println "testInsert..."
  let pt := PieceTable.fromString "Hello"
  -- Insert at end
  let pt1 := pt.insert 5 " World" 5
  assertEqual "Insert at end" "Hello World" pt1.toString
  -- Insert at middle
  let pt2 := pt1.insert 5 "," 5
  assertEqual "Insert at middle" "Hello, World" pt2.toString
  -- Insert at start
  let pt3 := pt2.insert 0 "Say: " 0
  assertEqual "Insert at start" "Say: Hello, World" pt3.toString
def testDelete : IO Unit := do
  IO.println "testDelete..."
  let pt := PieceTable.fromString "Hello, World!"
  -- Delete "World" (offset 7, len 5)
  let pt1 := pt.delete 7 5 7
  assertEqual "Delete middle" "Hello, !" pt1.toString
  -- Delete start
  let pt2 := pt1.delete 0 7 0
  assertEqual "Delete start" "!" pt2.toString
  -- Delete end
  let pt3 := pt2.delete 0 1 0
  assertEqual "Delete end" "" pt3.toString
def test : IO Unit := do
  IO.println "Starting PieceTable Basic Test..."
  testInsert
  testDelete
  IO.println "PieceTable Basic Test passed!"
end Test.PieceTable.Basic

import ViE.Data.PieceTable
import Test.Utils
open ViE
namespace Test.PieceTable.Appended
open Test.Utils
def testAppends : IO Unit := do
  IO.println "testAppends..."
  let pt := PieceTable.fromString "Line1\n"
  -- Append Line 2
  let pt1 := pt.insert pt.length "Line2\n" pt.length
  assertEqual "Append 1" "Line1\nLine2\n" pt1.toString
  -- Append Line 3
  let pt2 := pt1.insert pt1.length "Line3" pt1.length
  assertEqual "Append 2" "Line1\nLine2\nLine3" pt2.toString
def test : IO Unit := do
  IO.println "Starting PieceTable Appended Test..."
  testAppends
  IO.println "PieceTable Appended Test passed!"
end Test.PieceTable.Appended

import Test.Utils

open Test.Utils

def assert (msg : String) (cond : Bool) : IO Unit := do
  if !cond then
    throw (IO.userError s!"Assertion failed: {msg}")

  assertCursor "l moves right" s_l 0 1

  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)

  assert "h moves left" (s_lh.getCursor == Point.make 0 0)

  assertCursor "h moves left" s_lh 0 0

  assert "j moves down" (s_j.getCursor == Point.make 1 0)

  assertCursor "j moves down" s_j 1 0

  assert "k moves up" (s_jk.getCursor == Point.make 0 0)

  assertCursor "k moves up" s_jk 0 0

  -- 0, $

  assert "$ moves to end" (s_end.getCursor == Point.make 0 4) -- '1' is at col 4

  assertCursor "$ moves to end" s_end 0 4 -- '1' is at col 4

  assert "0 moves to start" (s_start.getCursor == Point.make 0 0)

  assertCursor "0 moves to start" s_start 0 0

  assert "w moves to next word" (s_w.getCursor == Point.make 0 6)

  assertCursor "w moves to next word" s_w 0 6

  assert "e moves to end of word" (s_e.getCursor == Point.make 0 4)

  assertCursor "e moves to end of word" s_e 0 4

  assert "we moves to end of next word" (s_we.getCursor == Point.make 0 10)

  assertCursor "we moves to end of next word" s_we 0 10

  assert "b moves to start of word" (s_web.getCursor == Point.make 0 6)

  assertCursor "b moves to start of word" s_web 0 6

  assert "G moves to last line" (s_G.getCursor.row == 2)

  assertCursor "G moves to last line" s_G 2 0

  assert "gg moves to first line" (s_gg.getCursor.row == 0)

  assertCursor "gg moves to first line" s_gg 0 0

  assert "| jumps to column" (s_pipe.getCursor.col == 2) -- 1-indexed count 3 -> col 2

  assertCursor "| jumps to column" s_pipe 0 2 -- 1-indexed count 3 -> col 2

  assert "i inserts" (s_i.getActiveBuffer.table.toString == "x")

  assertBuffer "i inserts" s_i "x"

  assert "a appends" (s_a.getActiveBuffer.table.toString == "xy")

  assertBuffer "a appends" s_a "xy"

  assert "A appends at end" (s_A.getActiveBuffer.table.toString == "xyz")

  assertBuffer "A appends at end" s_A "xyz"

  assert "o inserts line below" (s_o.getActiveBuffer.table.toString == "x\ny")

  assertBuffer "o inserts line below" s_o "x\ny"

  assert "O inserts line above" (s_O.getActiveBuffer.table.toString == "z\nx\ny")

  assertBuffer "O inserts line above" s_O "z\nx\ny"

  assert "x deletes char" (s_x.getActiveBuffer.table.toString == "")

  assertBuffer "x deletes char" s_x ""

  assert "dw deletes word" (s_dw.getActiveBuffer.table.toString == "world")

  assertBuffer "dw deletes word" s_dw "world"

  assert "cw changes word" (s_cw.getActiveBuffer.table.toString == "hi world")

  assertBuffer "cw changes word" s_cw "hi world"

  assert "dd deletes current line" (s_dd.getActiveBuffer.table.toString == "line1\nline3")

  assertBuffer "dd deletes current line" s_dd "line1\nline3"

  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")

  assertBuffer "p pastes below" s_p "line1\nline2\nline3\nline1\n"

  assert "P pastes above" (s_P.getActiveBuffer.table.toString == "line1\nline1\nline2\nline3")

  assertBuffer "P pastes above" s_P "line1\nline1\nline2\nline3"

  assert "visual d deletes selection" (s_v.getActiveBuffer.table.toString == "ghlight me")

  assertBuffer "visual d deletes selection" s_v "ghlight me"

  assert "visual y yanks selection" (s_vyp.getActiveBuffer.table.toString == "highlight me\nhighlight")

  assertBuffer "visual y yanks selection" s_vyp "highlight me\nhighlight"

  assert "3w moves 3 words" (s_3w.getCursor.col == 6) -- positions of 'a', 'b', 'c', 'd' start: 0, 2, 4, 6

  assertCursor "3w moves 3 words" s_3w 0 6

  -- 2dd

  -- 2j

  -- 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

  assert "2j moves 2 lines down" (s_2j.getCursor.row == 2)

  assertCursor "2j moves 2 lines down" s_2j 2 0

import Test.Utils

open Test.Utils

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}")

  let text1 := (s1.getActiveBuffer.table.toString)
  assert "Text after insert abc" (text1 == "abc")

  assertBuffer "Text after insert abc" s1 "abc"

  let text2 := (s2.getActiveBuffer.table.toString)
  assert "Text after undo" (text2 == "")
  -- Cursor check: Should be back at (0, 0)
  let c2 := s2.getCursor
  assert s!"Cursor after undo should be (0,0) but is ({c2.row.val}, {c2.col.val})" (c2.row.val == 0 && c2.col.val == 0)

  assertBuffer "Text after undo" s2 ""
  assertCursor "Cursor after undo should be (0,0)" s2 0 0

  let text3 := (s3.getActiveBuffer.table.toString)

  assert "Text after re-insert d" (text3 == "d")
  let c3 := s3.getCursor
  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)

  assertBuffer "Text after re-insert d" s3 "d"
  assertCursor "Cursor after insert 'd' and Esc should be (0,0)" s3 0 0

open ViE.PieceTable