[[lean_lib]]
name = "Test"

[[lean_exe]]
name = "test"
root = "Test"

  historyLimit : Nat := 100

  -- Use direct PieceTable insert for atomic undo

    modifyLineInBuffer buffer row fun line =>
      let chars := line.toList
      let newChars := (chars.take col) ++ [c] ++ (chars.drop col)
      String.ofList newChars

    match buffer.table.getOffsetFromPoint row col with
    | some offset => { buffer with table := buffer.table.insert offset (c.toString) offset
                                   dirty := true }
    | none => buffer

  let currentLine := getLine s.activeBufferContent row |>.getD ""
  let chars := currentLine.toList
  let beforeSplit := String.ofList (chars.take col)
  let afterSplit := String.ofList (chars.drop col)

  let s' := s.updateActiveBufferContent fun buffer =>
    let beforeLines := arrayTake buffer row
    let afterLines := arrayDrop buffer (row + 1)
    arrayConcat [beforeLines, #[stringToLine beforeSplit, stringToLine afterSplit], afterLines]

  -- Use direct PieceTable insert for atomic undo
  let s' := s.updateActiveBuffer fun buffer =>
    match buffer.table.getOffsetFromPoint row col with
    | some offset => { buffer with table := buffer.table.insert offset "\n" offset
                                   dirty := true }
    | none => buffer

    let s' := s.updateActiveBufferContent fun buffer =>
      modifyLine buffer row fun line =>
        let chars := line.toList
        let newChars := (chars.take (col - 1)) ++ (chars.drop col)
        String.ofList newChars

    let s' := s.updateActiveBuffer fun buffer =>
       match buffer.table.getOffsetFromPoint row (col - 1) with
       | some offset =>
            { buffer with table := buffer.table.delete offset 1 (offset + 1)
                          dirty := true }
       | none => buffer

    -- At start of line: join with previous line

    -- Join with previous line (delete previous newline)

    let prevLine := getLine s.activeBufferContent prevRow |>.getD ""
    let currentLine := getLine s.activeBufferContent row |>.getD ""
    let mergedLine := prevLine ++ currentLine
    let newCol := prevLine.length

    let s' := s.updateActiveBufferContent fun buffer =>
      let beforeLines := arrayTake buffer prevRow
      let afterLines := arrayDrop buffer (row + 1)
      arrayConcat [beforeLines, #[stringToLine mergedLine], afterLines]

    let s' := s.updateActiveBuffer fun buffer =>
       -- Verify we are deleting the newline at the end of prevRow.
       match buffer.table.getLineRange prevRow with
       | some (start, len) =>
          -- Newline is at start + len. Length of newline is 1 (for \n).
          -- Check EOL consistency?
          -- cursor for undo should be at start+len (before newline)
          { buffer with table := buffer.table.delete (start + len) 1 (start + len)
                        dirty := true }
       | none => buffer

    -- Cursor moves to end of previous line
    let newCol := (getLine s.activeBufferContent prevRow).map String.length |>.getD 0

  let s' := s.updateActiveBufferContent fun (buffer : TextBuffer) => deleteLine buffer cursor.row.val

  let row := cursor.row.val
  let s' := s.updateActiveBuffer fun buffer =>
    match buffer.table.getLineRange row with
    | some (start, len) =>
       let deleteLen := if row < FileBuffer.lineCount buffer - 1 then len + 1 else len
       -- Restore cursor at start of line
       { buffer with table := buffer.table.delete start deleteLen start
                     dirty := true }
    | none => buffer
  -- Reset cursor logic

  let newRow := min cursor.row.val (newBuffer.size.pred)

  let newRow := min row (newBuffer.size.pred)

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

    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 s' := s.updateActiveBuffer fun buffer =>
      -- Determine insert offset.
      -- Try start of next line. If EOF, append.
      let offset := match buffer.table.getOffsetFromPoint (row + 1) 0 with
                    | some off => off
                    | none => buffer.table.tree.length
      -- For paste, undo should restore cursor to insertion point
      -- Break undo grouping to ensure separate paste operations are distinct
      let pt := buffer.table.commit
      { buffer with table := pt.insert offset text offset
                    dirty := true }
    s'.setCursor (Point.make (row + 1) 0)

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

    let row := cursor.row.val
    let text := String.intercalate "\n" (lines.toList.map fun l => String.ofList l.toList) ++ "\n"
    let s' := s.updateActiveBuffer fun buffer =>
      let offset := match buffer.table.getOffsetFromPoint row 0 with
                     | some off => off
                     | none => 0
       let pt := buffer.table.commit
       { buffer with table := pt.insert offset text offset
                     dirty := true }
    s'.setCursor (Point.make row 0)
def EditorState.undo (s : EditorState) : EditorState :=
  -- Capture current cursor offset (if valid) for redo
  let buf := s.getActiveBuffer
  let currentOffset := match buf.table.getOffsetFromPoint s.getCursor.row.val s.getCursor.col.val with
                       | some off => off
                       | none => 0

  let (newTable, cursorOpt) := buf.table.undo currentOffset
  let s' := s.updateActiveBuffer fun _ => { buf with table := newTable, dirty := true }
  match cursorOpt with
  | some off =>
      let (r, c) := newTable.getPointFromOffset off
      let s'' := s'.setCursor (Point.make r c)
      { s'' with message := "Undo" }
  | none => { s' with message := "Already at oldest change" }
def EditorState.redo (s : EditorState) : EditorState :=
  -- Capture current cursor offset
  let buf := s.getActiveBuffer
  let currentOffset := match buf.table.getOffsetFromPoint s.getCursor.row.val s.getCursor.col.val with
                       | some off => off
                       | none => 0
  let (newTable, cursorOpt) := buf.table.redo currentOffset
  let s' := s.updateActiveBuffer fun _ => { buf with table := newTable, dirty := true }
  match cursorOpt with
  | some off =>
      let (r, c) := newTable.getPointFromOffset off
      let s'' := s'.setCursor (Point.make r c)
      { s'' with message := "Redo" }
  | none => { s' with message := "Already at newest change" }

  | Key.char 'u' => pure $ s.undo
  | Key.ctrl 'r' => pure $ s.redo

    { original := bytes, add := ByteArray.empty, tree := PieceTree.empty }

    { original := bytes, add := ByteArray.empty, tree := PieceTree.empty, undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }

    { original := bytes, add := ByteArray.empty, tree := tree }

    { original := bytes, add := ByteArray.empty, tree := tree, undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }

def PieceTable.insert (pt : PieceTable) (offset : Nat) (text : String) : PieceTable :=

def PieceTable.insert (pt : PieceTable) (offset : Nat) (text : String) (cursorOffset : Nat) : PieceTable :=

    { pt' with tree := newTree }

    -- Check optimization/merge compatibility
    let (finalUndoStack, newLastInsert) :=
      match pt.lastInsert with
      | some (lastOff, lastAddOff) =>
        if offset == lastOff && lastAddOff == pt.add.size then
          -- MERGE: Contiguous edit in doc and add buffer.
          -- Don't push to undoStack (reuse previous state as undo point)
          (pt.undoStack, some (offset + text.utf8ByteSize, lastAddOff + text.utf8ByteSize))
        else
          -- NO MERGE: Push current state
          let stack := (pt.tree, cursorOffset) :: pt.undoStack
          let params := if stack.length > pt.undoLimit then stack.take pt.undoLimit else stack
          (params, some (offset + text.utf8ByteSize, pt.add.size + text.utf8ByteSize))
      | none =>
          let stack := (pt.tree, cursorOffset) :: pt.undoStack
          let params := if stack.length > pt.undoLimit then stack.take pt.undoLimit else stack
          (params, some (offset + text.utf8ByteSize, pt.add.size + text.utf8ByteSize))
    { pt' with
      tree := newTree
      undoStack := finalUndoStack
      redoStack := []
      lastInsert := newLastInsert
    }

def PieceTable.delete (pt : PieceTable) (offset : Nat) (length : Nat) : PieceTable :=

def PieceTable.delete (pt : PieceTable) (offset : Nat) (length : Nat) (cursorOffset : Nat) : PieceTable :=

    { pt with tree := newTree }

    let stack := (pt.tree, cursorOffset) :: pt.undoStack
    let finalStack := if stack.length > pt.undoLimit then stack.take pt.undoLimit else stack
    { pt with
      tree := newTree
      undoStack := finalStack
      redoStack := []
      lastInsert := none -- Break merge chain
    }
/-- Commit the current edit group, forcing the next insert to start a new undo item. -/
def PieceTable.commit (pt : PieceTable) : PieceTable :=
  { pt with lastInsert := none }
/-- Undo the last operation -/
def PieceTable.undo (pt : PieceTable) (currentCursor : Nat) : PieceTable × Option Nat :=
  match pt.undoStack with
  | [] => (pt, none)
  | (prev, prevCursor) :: rest =>
    ({ pt with
      tree := prev
      undoStack := rest
      redoStack := (pt.tree, currentCursor) :: pt.redoStack
      lastInsert := none
    }, some prevCursor)
/-- Redo the last undone operation -/
def PieceTable.redo (pt : PieceTable) (currentCursor : Nat) : PieceTable × Option Nat :=
  match pt.redoStack with
  | [] => (pt, none)
  | (next, nextCursor) :: rest =>
    ({ pt with
      tree := next
      undoStack := (pt.tree, currentCursor) :: pt.undoStack
      redoStack := rest
      lastInsert := none
    }, some nextCursor)

/-- Get byte offset from Row/Col position -/
def PieceTable.getOffsetFromPoint (pt : PieceTable) (row col : Nat) : Option Nat :=
  match PieceTable.getLineRange pt row with
  | some (startOff, len) =>
      -- Allow col up to len (inclusive) for appending at end of line
      if col <= len then some (startOff + col)
      else if col == len + 1 then some (startOff + len) -- Lenient for cursor logic? No, strict.
      else some (startOff + len) -- Clamp to end of line if strictly greater? Better to be safe.
  | none => none

def PieceTable.lineCount (pt : PieceTable) : Nat :=
  match pt.tree with
  | .leaf _ s => s.lines + 1
  | .internal _ s => s.lines + 1
  | .empty => 1
partial def PieceTable.findLineForOffset (pt : PieceTable) (target : Nat) (low high : Nat) : Option (Nat × Nat) :=
  if low > high then none
  else
    let mid := (low + high) / 2
    match pt.getLineRange mid with
    | some (start, len) =>
      let endOff := start + len
      if target >= start && target <= endOff then
        some (mid, target - start)
      else if target < start then
         if mid == 0 then none
         else PieceTable.findLineForOffset pt target low (mid - 1)
      else
         PieceTable.findLineForOffset pt target (mid + 1) high
    | none => none
def PieceTable.getPointFromOffset (pt : PieceTable) (offset : Nat) : (Nat × Nat) :=
  match PieceTable.findLineForOffset pt offset 0 pt.lineCount with
  | some (r, c) => (r, c)
  | none => (0, 0) -- Fallback

  undoStack : List (PieceTree × Nat) := []
  redoStack : List (PieceTree × Nat) := []
  undoLimit : Nat := 100
  lastInsert : Option (Nat × Nat) := none

    grind only [internal.sizeOf_spec, Array.mk.sizeOf_spec]

    grind only [= internal.sizeOf_spec, = Array.mk.sizeOf_spec]

def cmdUndo (_ : List String) (state : EditorState) : IO EditorState :=
  return ViE.EditorState.undo state
def cmdRedo (_ : List String) (state : EditorState) : IO EditorState :=
  return ViE.EditorState.redo state

  ("undo", cmdUndo),
  ("u", cmdUndo),
  ("redo", cmdRedo),

        let buf := { loadedBuf with id := id }

        let buf := { loadedBuf with
          id := id
          table := { loadedBuf.table with undoLimit := state.config.historyLimit }
        }

        let table' := buffer.table.delete startOffset length
        let table'' := table'.insert startOffset newLine

        let table' := buffer.table.delete startOffset length startOffset
        let table'' := table'.insert startOffset newLine startOffset

import Test.Undo
import Test.Buffer
import Test.Layout
import Test.Integration
def main : IO Unit := do
  IO.println "Running all tests..."
  Test.Undo.test
  Test.Buffer.test
  Test.Layout.test
  Test.Integration.test
  IO.println "All tests finished."

import ViE.Data.PieceTable
open ViE.PieceTable
namespace Test.Undo
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}")
def test : IO Unit := do
  IO.println "Starting Undo/Redo Test..."
  -- 1. Create initial buffer
  let initialText := "Hello, World!"
  let pt0 := PieceTable.fromString initialText
  assert "Initial text correct" (pt0.toString == initialText)
  assert "Initial undo stack empty" (pt0.undoStack.isEmpty)
  -- 2. Insert " New" at end
  -- "Hello, World! New"
  let pt1 := pt0.insert 13 " New" 13
  assert "Text after insert" (pt1.toString == "Hello, World! New")
  assert "Undo stack has 1 item" (pt1.undoStack.length == 1)
  -- 3. Delete ", World"
  -- "Hello! New"
  -- "Hello, World!" -> offset 5, delete 7 (", World")
  let pt2 := pt1.delete 5 7 5
  assert "Text after delete" (pt2.toString == "Hello! New")
  assert "Undo stack has 2 items" (pt2.undoStack.length == 2)
  -- 4. Undo Modify (Delete)
  -- Should revert to "Hello, World! New"
  let (pt3, _) := pt2.undo 0
  assert "Text after undo delete" (pt3.toString == "Hello, World! New")
  assert "Undo stack has 1 item" (pt3.undoStack.length == 1)
  assert "Redo stack has 1 item" (pt3.redoStack.length == 1)
  -- 5. Undo Insert
  -- Should revert to "Hello, World!"
  let (pt4, _) := pt3.undo 0
  assert "Text after undo insert" (pt4.toString == "Hello, World!")
  assert "Undo stack has 0 items" (pt4.undoStack.isEmpty)
  assert "Redo stack has 2 items" (pt4.redoStack.length == 2)
  -- 6. Redo Insert
  -- Should go to "Hello, World! New"
  let (pt5, _) := pt4.redo 0
  assert "Text after redo insert" (pt5.toString == "Hello, World! New")
  assert "Undo stack has 1 item" (pt5.undoStack.length == 1)
  assert "Redo stack has 1 item" (pt5.redoStack.length == 1)
  -- 7. Redo Delete
  -- Should go to "Hello! New"
  let (pt6, _) := pt5.redo 0
  assert "Text after redo delete" (pt6.toString == "Hello! New")
  assert "Undo stack has 2 items" (pt6.undoStack.length == 2)
  assert "Redo stack empty" (pt6.redoStack.isEmpty)
  -- 8. Test Redo clearing on new edit
  let (pt7, _) := pt6.undo 0 -- "Hello, World! New"
  -- Insert " Again" at end -> "Hello, World! New Again"
  let pt8 := pt7.insert 17 " Again" 17
  assert "Text after new insert" (pt8.toString == "Hello, World! New Again")
  assert "Redo stack cleared" (pt8.redoStack.isEmpty)
  -- 9. Test Optimization (Grouping)
  -- Force break merge chain from previous step to ensure " 1" starts a new group
  let pt8_clean := { pt8 with lastInsert := none }
  let pt9 := pt8_clean.insert 23 " 1" 23 -- "Hello, World! New Again 1"
  let pt10 := pt9.insert 25 "2" 25 -- "Hello, World! New Again 12"
  let pt11 := pt10.insert 26 "3" 26 -- "Hello, World! New Again 123"
  assert "Text after group insert" (pt11.toString == "Hello, World! New Again 123")
  -- Should have only 1 new undo item for " 123" because they overlap
  -- pt8 had some undo stack. pt9 added 1. pt10 merged. pt11 merged.
  -- So pt11.undoStack.length should be pt8.undoStack.length + 1
  assert "Undo stack grouped" (pt11.undoStack.length == pt8.undoStack.length + 1)
  let (pt12, _) := pt11.undo 0
  assert "Undo removes group" (pt12.toString == "Hello, World! New Again")
  -- 10. Test Limit
  -- Force a small limit
  let ptLimit := { pt12 with undoLimit := 2 }
  let ptL1 := (ptLimit.insert 0 "A" 0) -- Stack: 1
  let ptL2 := (ptL1.insert 0 "B" 0) -- Stack: 2
  -- Previous insert was "A" at 0. LastInsert = (0 + 1, addOffset + 1).
  -- Current insert at 0. 0 != 1. So NOT contiguous. Correct.
  let ptL3 := (ptL2.insert 0 "C" 0) -- Stack: 3 -> capped to 2
  assert "Undo limit respected" (ptL3.undoStack.length == 2)
  -- The oldest undo (for "A") should be dropped. The remaining undos are "C" -> "B", and "B" -> "A".
  -- So undoing twice should start with "CBA..." -> "BA..." -> "A..."
  let (u1, _) := ptL3.undo 0
  let (u2, _) := u1.undo 0
  assert "Oldest undo dropped" (u2.toString == "AHello, World! New Again")
  assert "Oldest undo dropped" (u2.toString == "AHello, World! New Again")
  -- 11. Test Paste Undo Grouping (Reproduction)
  -- Scenario: Paste "P1" then Paste "P2". They should NOT merge if we signal a break,
  -- OR if we consider pastes as distinct operations that shouldn't auto-merge like typing.
  -- Currently PieceTable merges ANY contiguous insert.
  let ptBase := PieceTable.fromString ""
  let ptP1 := ptBase.insert 0 "P1" 0 -- Simulate Paste 1
  -- Simulate EditorState.paste calling commit before next insert
  let ptP1_committed := ptP1.commit
  let ptP2 := ptP1_committed.insert 2 "P2" 2 -- Simulate Paste 2 (contiguous)
  assert "Text is P1P2" (ptP2.toString == "P1P2")
  -- Expectation: 2 undo items (one for P1, one for P2).
  -- Bug: they merge into 1 item because offset 2 == lastInsert end.
  if ptP2.undoStack.length == 1 then
     IO.println "[FAIL] Paste operations merged (expected 2 undo items)"
     assert "Paste should not merge" false
  else
     IO.println "[PASS] Paste operations distinct (2 undo items)"
  IO.println "TestUndo passed!"
end Test.Undo

import ViE.Types
open ViE
namespace Test.Layout
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}")
def test : IO Unit := do
  IO.println "Starting Layout Test..."
  -- 1. Construct Layouts
  let view1 : ViewState := { bufferId := 1, cursor := {row:=0, col:=0}, scrollRow:=0, scrollCol:=0 }
  let win1 := Layout.window 1 view1
  let view2 : ViewState := { bufferId := 2, cursor := {row:=0, col:=0}, scrollRow:=0, scrollCol:=0 }
  let win2 := Layout.window 2 view2
  -- 2. Test Split Construction
  let hsplit := Layout.hsplit win1 win2 0.5
  match hsplit with
  | .hsplit l r ratio =>
      assert "HSplit match" true
      assert "HSplit ratio" (ratio == 0.5)
  | _ => assert "HSplit construction failed" false
  let vsplit := Layout.vsplit hsplit win1 0.3
  match vsplit with
  | .vsplit t b ratio =>
      assert "VSplit match" true
      assert "VSplit ratio" (ratio == 0.3)
      match t with
      | .hsplit _ _ _ => assert "VSplit top is HSplit" true
      | _ => assert "VSplit top incorrect" false
  | _ => assert "VSplit construction failed" false
  IO.println "LayoutTest passed!"
end Test.Layout

import ViE.Types
import ViE.State.Config
import ViE.Config
import ViE.Key.Map
import ViE.Command.Impl
open ViE
namespace Test.Integration
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
-- Helper: Convert string to list of char keys
def keys (s : String) : List Key :=
  s.toList.map Key.char
def test : IO Unit := do
  IO.println "Starting Integration Test..."
  -- Test 1: Typing "abc" -> Undo -> Insert "d"
  -- Expected: "abc" -> "" -> "d"
  -- Bug Report: After Undo, Insert mode might fail or buffer might be corrupted
  let s0 := ViE.initialState
  -- 1. Insert "abc"
  -- i a b c Esc
  let input1 := [Key.char 'i'] ++ keys "abc" ++ [Key.esc]
  let s1 ← runKeys s0 input1
  let text1 := (s1.getActiveBuffer.table.toString)
  assert "Text after insert abc" (text1 == "abc")
  -- 2. Undo
  -- u
  let s2 ← runKeys s1 [Key.char 'u']
  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)
  -- 3. Insert "d"
  -- i d Esc
  let s3 ← runKeys s2 [Key.char 'i', Key.char 'd', Key.esc]
  let text3 := (s3.getActiveBuffer.table.toString)
  assert "Text after re-insert d" (text3 == "d")
  let c3 := s3.getCursor
  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)
  IO.println "IntegrationTest passed!"
end Test.Integration

import ViE.Buffer.Content
import ViE.Types
import ViE.Data.PieceTable
open ViE
open ViE.PieceTable
namespace Test.Buffer
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}")
def test : IO Unit := do
  IO.println "Starting Buffer Test..."
  -- 1. Test fromString and getLine
  let text := "Hello\nWorld"
  let pt := PieceTable.fromString text
  let buf : FileBuffer := { initialFileBuffer with table := pt }
  -- Check lines
  match getLineFromBuffer buf 0 with
  | some l => assert "Line 0 is Hello" (l == "Hello")
  | none => assert "Line 0 missing" false
  match getLineFromBuffer buf 1 with
  | some l => assert "Line 1 is World" (l == "World")
  | none => assert "Line 1 missing" false
  match getLineFromBuffer buf 2 with
  | some _ => assert "Line 2 should be missing" false
  | none => assert "Line 2 correctly missing" true
  -- 2. Test FileBuffer <-> TextBuffer conversion
  let tb : TextBuffer := #[ #['A', 'B'], #['C'] ] -- "AB\nC"
  let buf2 := ViE.Buffer.fileBufferFromTextBuffer 1 (some "test.txt") tb
  assert "Buffer created from TextBuffer id" (buf2.id == 1)
  assert "Buffer created from TextBuffer filename" (buf2.filename == some "test.txt")
  let tb2 := ViE.Buffer.fileBufferToTextBuffer buf2
  assert "Roundtrip TextBuffer size" (tb2.size == 2)
  if tb2.size == 2 then
    let l0 := tb2[0]!
    let l1 := tb2[1]!
    assert "Roundtrip Line 0" (String.ofList l0.toList == "AB")
    assert "Roundtrip Line 1" (String.ofList l1.toList == "C")
  IO.println "BufferTest passed!"
end Test.Buffer