leanprover/lean4:v4.27.0

name = "vie"
version = "0.1.0"
defaultTargets = ["vie"]
[[lean_lib]]
name = "ViE"
[[lean_exe]]
name = "vie"
root = "Main"

{"version": "1.1.0",
 "packagesDir": ".lake/packages",
 "packages": [],
 "name": "editor",
 "lakeDir": ".lake"}

-- This module serves as the root of the `Editor` library.
-- Import modules here that should be built as part of the library.
import ViE.Basic
import ViE.Types
import ViE.Buffer
import ViE.Actions
import ViE.Command
import ViE.Key
import ViE.State
import ViE.Terminal
import ViE.UI
import ViE.IO
import ViE.Config
import ViE.App
import ViE.Loader
import ViE.Workspace

import ViE.Types
namespace ViE
/-- Resolve a file path relative to workspace -/
def Workspace.resolvePath (ws : Workspace) (path : String) : String :=
  if path.startsWith "/" then
    -- Absolute path, use as-is
    path
  else
    -- Relative path, resolve from workspace
    match ws.rootPath with
    | some root => root ++ "/" ++ path
    | none => path  -- No workspace, use as-is
end ViE

import ViE.Types
import ViE.Buffer
namespace ViE.Window
open ViE
def getAllWindowBounds (l : Layout) (h w : Nat) : List (Nat × Nat × Nat × Nat × Nat) :=
  let rec traverse (l : Layout) (r c h w : Nat) (acc : List (Nat × Nat × Nat × Nat × Nat)) : List (Nat × Nat × Nat × Nat × Nat) :=
    match l with
    | Layout.window id _ => (id, r, c, h, w) :: acc
    | Layout.hsplit left right ratio =>
      let leftW := (Float.ofNat w * ratio).toUInt64.toNat
      let acc' := traverse left r c h leftW acc
      traverse right r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0) acc'
    | Layout.vsplit top bottom ratio =>
      let topH := (Float.ofNat h * ratio).toUInt64.toNat
      let acc' := traverse top r c topH w acc
      traverse bottom (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w acc'
  traverse l 0 0 h w []
def getWindowIds (l : Layout) : List Nat :=
  match l with
  | Layout.window id _ => [id]
  | Layout.hsplit left right _ => getWindowIds left ++ getWindowIds right
  | Layout.vsplit top bottom _ => getWindowIds top ++ getWindowIds bottom

import ViE.State
import ViE.Types
import ViE.Window.Analysis
namespace ViE.Window
open ViE
def switchWindow (state : EditorState) (dir : Direction) : EditorState :=
  let wg := state.getCurrentWorkgroup
  let bounds := ViE.Window.getAllWindowBounds wg.layout (if state.windowHeight > 0 then state.windowHeight - 1 else 0) state.windowWidth
  let current := bounds.find? (fun (id, _, _, _, _) => id == wg.activeWindowId)
  match current with
  | none => state
  | some (_, r, c, h, w) =>
    -- Find candidates with orthogonal overlap
    let candidates := bounds.filter fun (id, r', c', h', w') =>
      id != wg.activeWindowId &&
      match dir with
      | .left => c' < c && (r' < r + h && r' + h' > r)
      | .right => c' >= c + w && (r' < r + h && r' + h' > r)
      | .up => r' < r && (c' < c + w && c' + w' > c)
      | .down => r' >= r + h && (c' < c + w && c' + w' > c)
    -- Filter again for adjacency/overlap
    let best := candidates.foldl (fun acc p =>
      let (_, r', c', _, _) := p
      match acc with
      | none => some p
      | some (_, br, bc, _, _) =>
         match dir with
         | .left => if c' > bc then some p else some acc.get!
         | .right => if c' < bc then some p else some acc.get!
         | .up => if r' > br then some p else some acc.get!
         | .down => if r' < br then some p else some acc.get!
    ) none
    match best with
    | some (id, _, _, _, _) => state.updateCurrentWorkgroup fun wg => { wg with activeWindowId := id }
    | none => state
def closeActiveWindow (state : EditorState) : EditorState :=
  let wg := state.getCurrentWorkgroup
  match wg.layout.remove wg.activeWindowId with
  | none => { state with shouldQuit := true }
  | some newLayout =>
    state.updateCurrentWorkgroup fun wg =>
      let newIds := ViE.Window.getWindowIds newLayout
      let newActiveId := match newIds with
        | [] => 0 -- Should not happen if layout valid
        | h :: _ => h
      { wg with layout := newLayout, activeWindowId := newActiveId }
def splitWindow (state : EditorState) (direction : Bool) : EditorState :=
  -- direction: true = vertical (top/bottom), false = horizontal (left/right)
  let s' := state.updateCurrentWorkgroup fun wg =>
    let activeId := wg.activeWindowId
    let nextId := wg.nextWindowId
    let currentView := wg.layout.findView activeId |>.getD initialView
    let newView := currentView
    let rec updateLayout (l : Layout) : Layout :=
      match l with
      | Layout.window wid v =>
        if wid == activeId then
          if direction then Layout.vsplit (Layout.window wid v) (Layout.window nextId newView) 0.5
          else Layout.hsplit (Layout.window wid v) (Layout.window nextId newView) 0.5
        else Layout.window wid v
      | Layout.hsplit left right r => Layout.hsplit (updateLayout left) (updateLayout right) r
      | Layout.vsplit top bottom r => Layout.vsplit (updateLayout top) (updateLayout bottom) r
    { wg with layout := updateLayout wg.layout, nextWindowId := nextId + 1 }
  { s' with message := "Split window" }
/-- Result of resize operation: None (not found), Some (layout, handled) -/
abbrev ResizeResult := Option (Layout × Bool)
def resizeWindow (state : EditorState) (dir : Direction) (amount : Float) : EditorState :=
  state.updateCurrentWorkgroup fun wg =>
    let activeId := wg.activeWindowId
    let rec traverse (l : Layout) : ResizeResult :=
      match l with
      | Layout.window wid v =>
        if wid == activeId then some (Layout.window wid v, false) else none
      | Layout.hsplit left right r =>
        match traverse left with
        | some (newLeft, handled) =>
          if handled then some (Layout.hsplit newLeft right r, true)
          else
            -- We are in left child, unhandled.
            match dir with
            | .left | .right => -- Horizontal resize
              let delta := if dir == .right then amount else -amount
              let newR := max 0.05 (min 0.95 (r + delta))
              some (Layout.hsplit newLeft right newR, true)
            | _ => some (Layout.hsplit newLeft right r, false)
        | none =>
          match traverse right with
          | some (newRight, handled) =>
            if handled then some (Layout.hsplit left newRight r, true)
            else
              -- We are in right child, unhandled.
              match dir with
              | .left | .right => -- Horizontal resize
                -- Consistent direction: Right (l) -> Increase ratio (move split right). Left (h) -> Decrease ratio (move split left).
                let delta := if dir == .right then amount else -amount
                let newR := max 0.05 (min 0.95 (r + delta))
                some (Layout.hsplit left newRight newR, true)
              | _ => some (Layout.hsplit left newRight r, false)
          | none => none
      | Layout.vsplit top bottom r =>
        match traverse top with
        | some (newTop, handled) =>
          if handled then some (Layout.vsplit newTop bottom r, true)
          else
            -- Top child
            match dir with
            | .up | .down => -- Vertical resize
               -- Top child: Down (j) -> Increase ratio (move split down). Up (k) -> Decrease ratio (move split up).
               let delta := if dir == .down then amount else -amount
               let newR := max 0.05 (min 0.95 (r + delta))
               some (Layout.vsplit newTop bottom newR, true)
            | _ => some (Layout.vsplit newTop bottom r, false)
        | none =>
          match traverse bottom with
          | some (newBottom, handled) =>
            if handled then some (Layout.vsplit top newBottom r, true)
            else
               -- Bottom child
               match dir with
               | .up | .down => -- Vertical resize
                 -- Bottom child: Down (j) -> Increase ratio (move split down). Up (k) -> Decrease ratio (move split up).
                 let delta := if dir == .down then amount else -amount
                 let newR := max 0.05 (min 0.95 (r + delta))
                 some (Layout.vsplit top newBottom newR, true)
               | _ => some (Layout.vsplit top newBottom r, false)
          | none => none
    match traverse wg.layout with
    | some (newLayout, _) => { wg with layout := newLayout }
    | none => wg
def cycleWindow (state : EditorState) : EditorState :=
  state.updateCurrentWorkgroup fun wg =>
    let ids := ViE.Window.getWindowIds wg.layout
    if ids.isEmpty then wg
    else
      let current := wg.activeWindowId
      -- Manual index search to avoid import issues if any
      let rec findNext (list : List Nat) (sawCurrent : Bool) : Option Nat :=
        match list with
        | [] => if sawCurrent then ids.head? else none
        | id :: rest =>
          if sawCurrent then some id
          else if id == current then findNext rest true
          else findNext rest false
      match findNext ids false with
      | some nextId => { wg with activeWindowId := nextId }
      | none => { wg with activeWindowId := match ids with | [] => wg.activeWindowId | h :: _ => h }
def enforceScroll (state : EditorState) : EditorState :=
  let (h, w) := state.getActiveWindowBounds
  -- Active window height. Reserve 1 line for status bar?
  -- UI logic reserves 1 for status bar in split rendering.
  let linesInView := if h > 1 then h - 1 else 1
  -- Vertical Scroll
  let (sRow, sCol) := state.getScroll
  let cursor := state.getCursor
  let state :=
    if cursor.row.val < sRow.val then
      state.setScroll cursor.row sCol
    else if cursor.row.val >= sRow.val + linesInView then
      let newScrollRow : Row := ⟨sRow.val + linesInView - 1⟩
      state.setScroll newScrollRow sCol
    else
      state
  -- Refresh scroll after potential update
  let (sRow, sCol) := state.getScroll
  -- Horizontal Scroll
  let lnWidth := if state.config.showLineNumbers then 4 else 0
  let colsInView := if w > lnWidth then w - lnWidth else 1
  let state :=
    if cursor.col.val < sCol.val then
      state.setScroll sRow cursor.col
    else if cursor.col.val >= sCol.val + colsInView then
      let newScrollCol : Col := ⟨sCol.val + colsInView - 1⟩
      state.setScroll sRow newScrollCol
    else
      state
  state
end ViE.Window

namespace ViE.Unicode
/-- Ranges of characters that have a visual width of 2 (Fullwidth/Wide).
    Based on EastAsianWidth.txt (Wide or Fullwidth). -/
def wideRanges : List (Nat × Nat) := [
  (0x1100, 0x115F), -- Hangul Jamo
  (0x2329, 0x232A), -- Angle brackets
  (0x2E80, 0x303E), -- CJK Radicals / Punctuation
  (0x3040, 0x3247), -- Hiragana, Katakana, Enclosed
  (0x3250, 0x4DBF), -- Enclosed CJK / CJK Extension A
  (0x4E00, 0xA4C6), -- CJK Unified Ideographs / Yi
  (0xA960, 0xA97C), -- Hangul Jamo Extended-A
  (0xAC00, 0xD7A3), -- Hangul Syllables
  (0xF900, 0xFAFF), -- CJK Compatibility Ideographs
  (0xFE10, 0xFE19), -- Vertical forms
  (0xFE30, 0xFE6F), -- CJK Compatibility Forms
  (0xFF01, 0xFF60), -- Fullwidth Forms
  (0xFFE0, 0xFFE6), -- Fullwidth currency/signs
  (0x1F300, 0x1F64F), -- Miscellaneous Symbols and Pictographs (Emojis)
  (0x1F900, 0x1F9FF)  -- Supplemental Symbols and Pictographs (some, generic range)
]
/-- Check if a character code is in a wide range. -/
def isWide (c : Nat) : Bool :=
  wideRanges.any fun (start, stop) => c >= start && c <= stop
/-- Get the visual width of a character.
    Returns 2 for wide characters, 0 for null/combining (simplified), 1 for others. -/
def charWidth (c : Char) : Nat :=
  let n := c.toNat
  if n == 0 then 0 -- Null is 0 width? Or usually displayed as something?
                 -- Usually invalid in text, but let's say 0.
  else if n < 0x20 then 2 -- Control characters shown as ^A
  else if n == 0x7F then 2 -- DEL shown as ^?
  else if isWide n then 2
  else 1
/-- Get the display string for a character.
    - Control characters (0x00-0x1F) -> "^A" notation.
    - 0x7F -> "^?"
    - Others -> character itself as string. -/
def getDisplayString (c : Char) : String :=
  let n := c.toNat
  if n < 0x20 then
    -- 0x01 is ^A (A is 0x41). 0x01 + 0x40 = 0x41.
    -- 0x00 is ^@.
    let base := (n + 0x40).toUInt8
    "^" ++ (Char.ofNat base.toNat).toString
  else if n == 0x7F then
    "^?"
  else
    c.toString
/-- Calculate the total visual width of a string. -/
def stringWidth (s : String) : Nat :=
  s.foldl (fun acc c => acc + charWidth c) 0
/-- Calculate the total visual width of a substring. -/
def substringWidth (s : Substring.Raw) : Nat :=
  s.foldl (fun acc c => acc + charWidth c) 0
/-- Get the byte length of a UTF-8 sequence starting with `b`.
    Returns 0 if `b` is a continuation byte or invalid start. -/
def utf8ByteLength (b : UInt8) : Nat :=
  if b < 0x80 then 1
  else if (b &&& 0xE0) == 0xC0 then 2
  else if (b &&& 0xF0) == 0xE0 then 3
  else if (b &&& 0xF8) == 0xF0 then 4
  else 0 -- Invalid or continuation
/-- Count newlines in a byte array slice efficiently -/
def countNewlines (data : ByteArray) (start : Nat) (len : Nat) : Nat :=
  let endPos := start + len
  let rec loop (i : Nat) (count : Nat) : Nat :=
    if i >= endPos then count
    else
      if data[i]! == 10 then loop (i + 1) (count + 1) -- 10 is \n
      else loop (i + 1) count
  loop start 0
/-- Count UTF-8 characters in a byte array range. -/
def countChars (bytes : ByteArray) (start len : Nat) : Nat :=
  let stop := start + len
  let rec loop (i : Nat) (cnt : Nat) : Nat :=
    if i >= stop then cnt
    else
      let b := bytes[i]!
      if (b &&& 0xC0) != 0x80 then
        loop (i + 1) (cnt + 1)
      else
        loop (i + 1) cnt
  loop start 0
end ViE.Unicode

import ViE.State
import ViE.Terminal
import ViE.Config
import ViE.Unicode
import ViE.Color
namespace ViE.UI
open ViE
/-- Pad a string on the left with spaces until it reaches the given width. -/
def leftPad (s : String) (width : Nat) : String :=
  if s.length >= width then s
  else "".pushn ' ' (width - s.length) ++ s
/-- Take characters from substring until visual width limit is reached. -/
partial def takeVisual (s : Substring.Raw) (width : Nat) : String :=
  let rec loop (sub : Substring.Raw) (currW : Nat) (acc : String) : String :=
    if sub.isEmpty then acc
    else
      let c := sub.front
      let w := Unicode.charWidth c
      if currW + w <= width then
        loop (sub.drop 1) (currW + w) (acc ++ Unicode.getDisplayString c)
      else
        acc
  loop s 0 ""
/-- Render the current editor state to the terminal. -/
def render (state : EditorState) : IO Unit := do
  -- Start building the frame buffer
  let mut buffer := ""
  buffer := buffer ++ Terminal.hideCursorStr ++ Terminal.homeCursorStr
  let (rows, cols) ← Terminal.getWindowSize
  let wg := state.getCurrentWorkgroup
  let getBuffer (id : Nat) : FileBuffer :=
    wg.buffers.find? (fun b => b.id == id) |>.getD initialBuffer
  let rec renderLayout (l : Layout) (r c h w : Nat) : String := Id.run do
    match l with
    | Layout.window id view =>
      let workH := if h > 0 then h - 1 else 0
      let buf := getBuffer view.bufferId
      let mut winBuf := ""
      for i in [0:workH] do
        let lineIdx := view.scrollRow + i
        let screenRow := r + i
        -- Position cursor for this line
        winBuf := winBuf ++ Terminal.moveCursorStr screenRow c
        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
             let sub := lineStr.toRawSubstring.drop view.scrollCol.val
             let displayLine := takeVisual sub availableWidth
             if state.config.showLineNumbers then
               winBuf := winBuf ++ s!"{leftPad (toString (lineIdx + 1)) 3} "
             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
               -- 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
                  winBuf := winBuf ++ c.toString
                  idx := idx + 1
               if styleActive then winBuf := winBuf ++ "\x1b[0m"
        else
           winBuf := winBuf ++ state.config.emptyLineMarker
        -- Clear the rest of the line to ensure clean overwrite
        winBuf := winBuf ++ Terminal.clearLineStr
      let statusRow := r + workH
      winBuf := winBuf ++ Terminal.moveCursorStr statusRow c
      let fileName := buf.filename.getD "[No Name]"
      let modeStr := if id == wg.activeWindowId then s!"-- {state.mode} --" else "--"
      let eolMark := if buf.missingEol then " [noeol]" 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
      -- Cursor drawing is separate (at end of frame)
      winBuf
    | Layout.hsplit left right ratio =>
      let leftW := (Float.ofNat w * ratio).toUInt64.toNat
      let leftStr := renderLayout left r c h leftW
      -- Draw vertical separator
      let mut sepStr := ""
      if w > leftW then
        let sepCol := c + leftW
        for i in [0:h] do
           sepStr := sepStr ++ Terminal.moveCursorStr (r + i) sepCol ++ state.config.vSplitStr
      let rightStr := renderLayout right r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0)
      leftStr ++ sepStr ++ rightStr
    | Layout.vsplit top bottom ratio =>
      let topH := (Float.ofNat h * ratio).toUInt64.toNat
      let topStr := renderLayout top r c topH w
      -- Draw horizontal separator
      let mut sepStr := ""
      if h > topH then
        let sepRow := r + topH
        sepStr := sepStr ++ Terminal.moveCursorStr sepRow c
        for _ in [0:w] do
           sepStr := sepStr ++ state.config.hSplitStr
      let bottomStr := renderLayout bottom (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w
      topStr ++ sepStr ++ bottomStr
  let layoutH := rows - 1
  buffer := buffer ++ renderLayout wg.layout 0 0 layoutH cols
  -- Global Status / Command Line
  buffer := buffer ++ Terminal.moveCursorStr (rows - 1) 0
  let statusRight :=
    if state.mode == .command then s!":{state.inputState.commandBuffer}"
    else state.message
  buffer := buffer ++ statusRight ++ Terminal.clearLineStr
  -- Set Physical Cursor
  let rec getCursorPos (l : Layout) (r c h w : Nat) : Option (Nat × Nat) :=
    match l with
    | Layout.window id view =>
      if id == wg.activeWindowId then
         let buf := getBuffer view.bufferId
         let workH := if h > 0 then h - 1 else 0
         let colOffset := if state.config.showLineNumbers then 4 else 0
         let visualRow := view.cursor.row.val - view.scrollRow.val
         if visualRow >= 0 && visualRow < workH then
             if let some currentLineStr := getLineFromBuffer buf view.cursor.row.val then
               let preCursor := (currentLineStr.toRawSubstring.drop view.scrollCol.val).take (view.cursor.col.val - view.scrollCol.val)
               let visualCol := ViE.Unicode.substringWidth preCursor
               if (visualCol + colOffset) < w then
                  some (r + visualRow, c + visualCol + colOffset)
               else none
             else none
         else none
      else none
    | Layout.hsplit left right ratio =>
      let leftW := (Float.ofNat w * ratio).toUInt64.toNat
      (getCursorPos left r c h leftW).orElse (fun _ => getCursorPos right r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0))
    | Layout.vsplit top bottom ratio =>
      let topH := (Float.ofNat h * ratio).toUInt64.toNat
      (getCursorPos top r c topH w).orElse (fun _ => getCursorPos bottom (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w)
  buffer := buffer ++
    match getCursorPos wg.layout 0 0 layoutH cols with
    | some (pr, pc) => Terminal.moveCursorStr pr pc
    | none => "" -- Cursor hidden or out of view
  if state.mode == .command then
     buffer := buffer ++ Terminal.moveCursorStr (rows - 1) (1 + state.inputState.commandBuffer.length)
  if state.mode == .visual || state.mode == .visualBlock then
    buffer := buffer ++ Terminal.hideCursorStr
  else
    buffer := buffer ++ Terminal.showCursorStr
  -- Output everything
  IO.print buffer
  (← IO.getStdout).flush
end ViE.UI

import ViE.Data.PieceTable
namespace ViE
open ViE.PieceTable
inductive Mode where
  | normal
  | insert
  | command
  | visual
  | visualBlock
  deriving Repr, BEq, Inhabited
instance : ToString Mode where
  toString
    | .normal => "NORMAL"
    | .insert => "INSERT"
    | .command => "COMMAND"
    | .visual => "VISUAL"
    | .visualBlock => "VISUAL BLOCK"
/-- Workspace configuration -/
structure Workspace where
  rootPath : Option String := none
  displayName : String := "Untitled"
deriving Repr
/-- Row index (0-based) with dimensional safety -/
structure Row where
  val : Nat
  deriving Repr, BEq, Ord
/-- Column index (0-based) with dimensional safety -/
structure Col where
  val : Nat
  deriving Repr, BEq, Ord
/-- Cursor position with dimensional type safety -/
structure Point where
  row : Row
  col : Col
  deriving Repr, BEq
-- Row helper functions
namespace Row
  def zero : Row := ⟨0⟩
  def succ (r : Row) : Row := ⟨r.val + 1⟩
  def pred (r : Row) : Row := ⟨r.val.pred⟩
  @[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 : ToString Row := ⟨fun r => toString r.val⟩
end Row
-- Col helper functions
namespace Col
  def zero : Col := ⟨0⟩
  def succ (c : Col) : Col := ⟨c.val + 1⟩
  def pred (c : Col) : Col := ⟨c.val.pred⟩
  @[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 : ToString Col := ⟨fun c => toString c.val⟩
end Col
-- Point helper functions
namespace Point
  def zero : Point := ⟨Row.zero, Col.zero⟩
  def make (row col : Nat) : Point := ⟨⟨row⟩, ⟨col⟩⟩
end Point
-- Inhabited instances
instance : Inhabited Row := ⟨Row.zero⟩
instance : Inhabited Col := ⟨Col.zero⟩
instance : Inhabited Point := ⟨Point.zero⟩
/-- A line is an array of characters for O(1) indexing -/
abbrev Line := Array Char
/-- A text buffer is an array of lines (2D character array) -/
abbrev TextBuffer := Array Line
structure EditorConfig where
  showLineNumbers : Bool
  vSplitStr : String
  hSplitStr : String
  emptyLineMarker : String
  statusBarStyle : String
  resetStyle : String
  fileIcon : String
  dirIcon : String
  deriving Repr, Inhabited
inductive Key where
  | char (c : Char)
  | ctrl (c : Char)
  | alt (c : Char)
  | esc
  | backspace
  | enter
  | left | right | up | down
  | unknown (c : Char)
  deriving Repr, BEq, Inhabited
structure FileBuffer where
  id : Nat
  filename : Option String
  dirty : Bool
  table : PieceTable
  missingEol : Bool
  deriving Inhabited
-- Manual Repr instance
instance : Repr FileBuffer where
  reprPrec buf _ :=
    s!"FileBuffer(id={buf.id}, file={buf.filename}, dirty={buf.dirty}, lines={PieceTree.lineBreaks buf.table.tree + 1})"
def initialFileBuffer : FileBuffer := {
  id := 0
  filename := none
  dirty := false
  table := PieceTable.fromString ""
  missingEol := false
}
namespace FileBuffer
  def lineCount (buf : FileBuffer) : Nat :=
    PieceTree.lineBreaks buf.table.tree + 1
end FileBuffer
structure ViewState where
  bufferId : Nat
  cursor : Point
  scrollRow : Row
  scrollCol : Col
  deriving Repr, Inhabited
/-- File entry for explorer -/
structure FileEntry where
  name : String
  path : String
  isDirectory : Bool
  deriving Repr, Inhabited
/-- Explorer state for file navigation -/
structure ExplorerState where
  currentPath : String
  entries : List FileEntry
  selectedIndex : Nat
  deriving Repr, Inhabited
inductive Layout where
  | window (id : Nat) (view : ViewState)
  | hsplit (left right : Layout) (ratio : Float)
  | vsplit (top bottom : Layout) (ratio : Float)
  deriving Repr, Inhabited
/-- Temporary input state that doesn't need to persist -/
structure InputState where
  previousKey : Option Char
  countBuffer : String
  commandBuffer : String
  pendingKeys : String
  lastInputTime : Nat
  deriving Repr, Inhabited
/-- State for a single workgroup (independent buffer set and layout) -/
structure WorkgroupState where
  buffers : List FileBuffer
  nextBufferId : Nat
  layout : Layout
  activeWindowId : Nat
  nextWindowId : Nat
  deriving Repr, Inhabited
structure EditorState where
  mode : Mode
  -- Workgroup management
  workgroups : Array WorkgroupState
  currentGroup : Nat
  -- Global State
  message : String
  shouldQuit : Bool
  config : EditorConfig
  workspace : Workspace
  clipboard : Option TextBuffer -- Yank buffer
  selectionStart : Option Point -- Visual mode anchor
  explorers : List (Nat × ExplorerState) -- BufferId × Explorer state
  -- Temporary input state
  inputState : InputState
  -- UI dimensions (updated frequently)
  windowHeight : Nat
  windowWidth : Nat
  -- Rendering optimization
  dirty : Bool
/-- Key mapping function type. -/
structure KeyMap where
  normal : EditorState → Key → IO EditorState
  insert : EditorState → Key → IO EditorState
  command : EditorState → Key → IO EditorState
  visual : EditorState → Key → IO EditorState
  visualBlock : EditorState → Key → IO EditorState
/-- Command action type: arguments -> state -> IO new state -/
abbrev CommandAction := List String → EditorState → IO EditorState
/-- Map of command names to actions -/
abbrev CommandMap := List (String × CommandAction)
/-- The complete user configuration. -/
structure Config where
  settings : EditorConfig
  bindings : KeyMap
  commands : CommandMap
inductive Direction where
  | left
  | right
  | up
  | down
  deriving Repr, BEq, Inhabited
structure SessionState where
  files : List String
  activeFileIndex : Nat
  cursors : List (Nat × Nat) -- Row, Col per file
  deriving Repr, Inhabited
end ViE

import ViE.Unicode
namespace ViE.Terminal
/-- Enable raw mode using stty.
    This relies on the availability of the `stty` command in the environment. -/
def enableRawMode : IO Unit := do
  -- We ignore the output.
  -- Explicitly target /dev/tty because IO.Process might redirect stdin
  -- min 0 time 0 for non-blocking read
  let _ ← IO.Process.run { cmd := "stty", args := #["-F", "/dev/tty", "raw", "-echo", "min", "0", "time", "0"] }
  return ()
/-- Disable raw mode using stty. -/
def disableRawMode : IO Unit := do
  let _ ← IO.Process.run { cmd := "stty", args := #["-F", "/dev/tty", "sane"] }
  return ()
/-- Clear the screen and position cursor at top-left. -/
def clearScreen : IO Unit := do
  IO.print "\x1b[2J"
  IO.print "\x1b[H"
/-- Get window size (rows, cols) using stty size. -/
def getWindowSize : IO (Nat × Nat) := do
  let out ← IO.Process.run { cmd := "stty", args := #["-F", "/dev/tty", "size"] }
  let parts := out.trimAscii.toString.splitOn " "
  match parts with
  | [rows, cols] =>
    let r := rows.toNat!
    let c := cols.toNat!
    return (r, c)
  | _ => return (24, 80) -- Fallback
/-- Move cursor to specific row and column (0-indexed). -/
def moveCursor (row col : Nat) : IO Unit := do
  -- ANSI escape codes are 1-indexed.
  IO.print s!"\x1b[{row + 1};{col + 1}H"
def moveCursorStr (row col : Nat) : String :=
  s!"\x1b[{row + 1};{col + 1}H"
/-- Hide cursor. -/
def hideCursor : IO Unit := do
  IO.print "\x1b[?25l"
def hideCursorStr : String := "\x1b[?25l"
/-- Show cursor. -/
def showCursor : IO Unit := do
  IO.print "\x1b[?25h"
def showCursorStr : String := "\x1b[?25h"
/-- Clear from cursor to end of line. -/
def clearLineStr : String := "\x1b[K"
/-- Home cursor. -/
def homeCursorStr : String := "\x1b[H"
/-- Read a single byte from stdin.
    Returns none on EOF or if no input available. -/
def readKey : IO (Option Char) := do
  let stdin ← IO.getStdin
  let b1_arr ← stdin.read 1
  if b1_arr.size == 0 then
    return none
  let b1 := b1_arr[0]!
  let len := ViE.Unicode.utf8ByteLength b1
  if len == 1 then
    return some (Char.ofNat b1.toNat)
  else if len == 0 then
    -- Invalid start byte, ignore
    return none
  else
    -- Read remaining bytes (blocking for completion of valid UTF-8 char)
    -- If we got the first byte of a multi-byte sequence, the rest should be there immediately.
    let rest ← stdin.read (len - 1).toUSize
    if rest.size != len - 1 then return none
    let b1n := b1.toNat
    if len == 2 then
        let b2 := rest[0]!.toNat
        let u := ((b1n &&& 0x1F) <<< 6) ||| (b2 &&& 0x3F)
        return some (Char.ofNat u)
    else if len == 3 then
        let b2 := rest[0]!.toNat
        let b3 := rest[1]!.toNat
        let u := ((b1n &&& 0x0F) <<< 12) ||| ((b2 &&& 0x3F) <<< 6) ||| (b3 &&& 0x3F)
        return some (Char.ofNat u)
    else if len == 4 then
        let b2 := rest[0]!.toNat
        let b3 := rest[1]!.toNat
        let b4 := rest[2]!.toNat
        let u := ((b1n &&& 0x07) <<< 18) ||| ((b2 &&& 0x3F) <<< 12) ||| ((b3 &&& 0x3F) <<< 6) ||| (b4 &&& 0x3F)
        return some (Char.ofNat u)
    else
        return none
end ViE.Terminal

import ViE.State.Config
import ViE.State.Edit
import ViE.State.Layout
import ViE.State.Movement
import ViE.State.Visual

import ViE.State.Config
import ViE.State.Layout
import ViE.State.Movement
import ViE.Types
import ViE.Buffer.Content
namespace ViE
def EditorState.startVisualMode (s : EditorState) : EditorState :=
  let s' := s.clampCursor
  { s' with mode := .visual, selectionStart := some s'.getCursor, message := "-- VISUAL --" }
def EditorState.startVisualBlockMode (s : EditorState) : EditorState :=
  let s' := s.clampCursor
  { s' with mode := .visualBlock, selectionStart := some s'.getCursor, message := "-- VISUAL BLOCK --" }
def EditorState.exitVisualMode (s : EditorState) : EditorState :=
  { s with mode := .normal, selectionStart := none, message := "" }
def normalizeRange (p1 p2 : Point) : (Point × Point) :=
  if p1.row < p2.row || (p1.row == p2.row && p1.col <= p2.col) then (p1, p2) else (p2, p1)
def EditorState.isInSelection (s : EditorState) (row col : Nat) : Bool :=
  match s.selectionStart with
  | none => false
  | some startPt =>
    if s.mode == .visualBlock then
       let cursor := s.getCursor
       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
       row >= minRow.val && row <= maxRow.val && col >= minCol.val && col <= maxCol.val
    else if s.mode == .visual then
       let (p1, p2) := normalizeRange startPt s.getCursor
       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
       else false
    else
       false
def EditorState.getSelectedText (s : EditorState) : TextBuffer :=
  match s.selectionStart with
  | none => #[]
  | some startPt =>
    if s.mode == .visualBlock then
      let cursor := s.getCursor
      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)))
    else
      let (p1, p2) := normalizeRange startPt s.getCursor
      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]]
def EditorState.yankSelection (s : EditorState) : EditorState :=
  let text := s.getSelectedText
  { s.exitVisualMode with clipboard := some text, message := s!"Yanked {text.size} lines" }
def EditorState.deleteSelection (s : EditorState) : EditorState :=
  match s.selectionStart with
  | none => s
  | some startPt =>
    if s.mode == .visualBlock then
      let cursor := s.getCursor
      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
    else
      let (p1, p2) := normalizeRange startPt s.getCursor
      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
end ViE

import ViE.State.Config
import ViE.State.Layout
import ViE.Types
import ViE.Buffer.Content
namespace ViE
def EditorState.getCursor (s : EditorState) : Point :=
  let wg := s.getCurrentWorkgroup
  match wg.layout.findView wg.activeWindowId with
  | some view => view.cursor
  | none => Point.zero
def EditorState.setCursor (s : EditorState) (p : Point) : EditorState :=
  s.updateActiveView fun v => { v with cursor := p }
def EditorState.setScroll (s : EditorState) (row : Row) (col : Col) : EditorState :=
  s.updateActiveView fun v => { v with scrollRow := row, scrollCol := col }
def EditorState.moveCursorLeft (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  -- let currentLine := getLine s.activeBufferContent cursor.row.val |>.getD ""
  if cursor.col.val > 0 then
     s.setCursor (Point.make cursor.row.val (cursor.col.val - 1))
  else
     s
def EditorState.moveCursorRight (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  let buffer := s.getActiveBuffer
  let limit := getLineLengthFromBuffer buffer cursor.row.val |>.getD 0
  if cursor.col.val < limit then
     s.setCursor (Point.make cursor.row.val (cursor.col.val + 1))
  else
     s
def EditorState.moveCursorUp (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  if cursor.row.val > 0 then
    let newRow := cursor.row.val - 1
    let lineLen := getLineLengthFromBuffer s.getActiveBuffer newRow |>.getD 0
    s.setCursor (Point.make newRow (min cursor.col.val lineLen))
  else
    s
def EditorState.moveCursorDown (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  let buffer := s.getActiveBuffer
  if cursor.row.val < buffer.lineCount - 1 then
    let newRow := cursor.row.val + 1
    let lineLen := getLineLengthFromBuffer buffer newRow |>.getD 0
    s.setCursor (Point.make newRow (min cursor.col.val lineLen))
  else
    s
def EditorState.clearInputState (s : EditorState) : EditorState :=
  { s with inputState := { s.inputState with countBuffer := "", previousKey := none } }
def EditorState.moveCursorLeftN (s : EditorState) (n : Nat) : EditorState :=
  n.repeat (fun s => s.moveCursorLeft) s
def EditorState.moveCursorRightN (s : EditorState) (n : Nat) : EditorState :=
  n.repeat (fun s => s.moveCursorRight) s
def EditorState.moveCursorUpN (s : EditorState) (n : Nat) : EditorState :=
  n.repeat (fun s => s.moveCursorUp) s
def EditorState.moveCursorDownN (s : EditorState) (n : Nat) : EditorState :=
  n.repeat (fun s => s.moveCursorDown) s
def EditorState.getCount (s : EditorState) : Nat :=
  match s.inputState.countBuffer.toNat? with
  | some n => n
  | none => 1
def EditorState.jumpToColumn (s : EditorState) (col : Nat) : EditorState :=
  let cursor := s.getCursor
  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)
  { s' with inputState := { s'.inputState with countBuffer := "" } }
def EditorState.jumpToLine (s : EditorState) (line : Nat) : EditorState :=
  let buffer := s.getActiveBuffer
  let maxLine := buffer.lineCount
  let newRow := if line == 0 then 0 else min (line - 1) (maxLine - 1)
  let lineLen := getLineLengthFromBuffer buffer newRow |>.getD 0
  let cursor := s.getCursor
  let newCol := min cursor.col.val lineLen
  let s' := s.setCursor (Point.make newRow newCol)
  { s' with inputState := { s'.inputState with countBuffer := "" } }
def EditorState.moveToLineStart (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  s.setCursor { cursor with col := 0 }
def EditorState.moveToLineEnd (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  let len := getLineLengthFromBuffer s.getActiveBuffer cursor.row.val |>.getD 0
  s.setCursor (Point.make cursor.row.val len)
def EditorState.clampCursor (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  let len := getLineLengthFromBuffer s.getActiveBuffer cursor.row.val |>.getD 0
  if cursor.col.val > len then
    s.setCursor (Point.make cursor.row.val len)
  else
    s
end ViE

import ViE.State.Config
import ViE.Types
import ViE.Buffer.Content
namespace ViE
/-- Get current workgroup -/
def EditorState.getCurrentWorkgroup (s : EditorState) : WorkgroupState :=
  s.workgroups[s.currentGroup]!
/-- Update current workgroup -/
def EditorState.updateCurrentWorkgroup (s : EditorState) (f : WorkgroupState → WorkgroupState) : EditorState :=
  { s with workgroups := s.workgroups.set! s.currentGroup (f (s.getCurrentWorkgroup)) }
/-- Switch to workgroup n -/
def EditorState.switchToWorkgroup (s : EditorState) (n : Nat) : EditorState :=
  if n < 10 then
    { s with currentGroup := n }
  else
    s
/- Helper functions to access/modify the active view -/
def Layout.findView (l : Layout) (id : Nat) : Option ViewState :=
  match l with
  | .window wid v => if wid == id then some v else none
  | .hsplit left right _ => (left.findView id).orElse (fun _ => right.findView id)
  | .vsplit top bottom _ => (top.findView id).orElse (fun _ => bottom.findView id)
/-- Update a view in the layout tree. Returns (updated layout, found flag) -/
def Layout.updateView (l : Layout) (id : Nat) (f : ViewState → ViewState) : Layout :=
  let rec update (l : Layout) : Layout × Bool :=
    match l with
    | .window wid v =>
      if wid == id then (.window wid (f v), true) else (l, false)
    | .hsplit left right ratio =>
      let (newLeft, found) := update left
      if found then
        (.hsplit newLeft right ratio, true)
      else
        let (newRight, found') := update right
        (.hsplit newLeft newRight ratio, found')
    | .vsplit top bottom ratio =>
      let (newTop, found) := update top
      if found then
        (.vsplit newTop bottom ratio, true)
      else
        let (newBottom, found') := update bottom
        (.vsplit newTop newBottom ratio, found')
  (update l).1
def Layout.remove (l : Layout) (id : Nat) : Option Layout :=
  match l with
  | .window wid _ => if wid == id then none else some l
  | .hsplit left right ratio =>
    match left.remove id with
    | none => some right
    | some newLeft =>
      match right.remove id with
      | none => some newLeft
      | some newRight => some (.hsplit newLeft newRight ratio)
  | .vsplit top bottom ratio =>
    match top.remove id with
    | none => some bottom
    | some newTop =>
      match bottom.remove id with
      | none => some newTop
      | some newBottom => some (.vsplit newTop newBottom ratio)
def EditorState.getActiveBuffer (s : EditorState) : FileBuffer :=
  let wg := s.getCurrentWorkgroup
  match wg.layout.findView wg.activeWindowId with
  | some v => wg.buffers.find? (fun b => b.id == v.bufferId) |>.getD initialBuffer
  | none => initialBuffer
def EditorState.activeBufferContent (s : EditorState) : TextBuffer :=
  ViE.Buffer.fileBufferToTextBuffer s.getActiveBuffer
def EditorState.updateActiveBuffer (s : EditorState) (f : FileBuffer -> FileBuffer) : EditorState :=
  s.updateCurrentWorkgroup fun wg =>
    let view := wg.layout.findView wg.activeWindowId
    match view with
    | some v =>
      let newBuffers := wg.buffers.map fun b => if b.id == v.bufferId then f b else b
      { wg with buffers := newBuffers }
    | none => wg
def EditorState.updateActiveBufferContent (s : EditorState) (f : TextBuffer → TextBuffer) : EditorState :=
  s.updateActiveBuffer fun b => ViE.Buffer.fileBufferUpdateFromTextBuffer b (f (ViE.Buffer.fileBufferToTextBuffer b))
def EditorState.getScroll (s : EditorState) : Row × Col :=
  let wg := s.getCurrentWorkgroup
  match wg.layout.findView wg.activeWindowId with
  | some v => (v.scrollRow, v.scrollCol)
  | none => (Row.zero, Col.zero)
def EditorState.updateActiveView (s : EditorState) (f : ViewState → ViewState) : EditorState :=
  s.updateCurrentWorkgroup fun wg =>
    { wg with layout := wg.layout.updateView wg.activeWindowId f }
def EditorState.getActiveWindowBounds (s : EditorState) : Nat × Nat :=
  let wg := s.getCurrentWorkgroup
  let rec findBounds (l : Layout) (h w : Nat) : Option (Nat × Nat) :=
    match l with
    | .window id _ => if id == wg.activeWindowId then some (h, w) else none
    | .hsplit left right ratio =>
      let leftW := (Float.ofNat w * ratio).toUInt64.toNat
      (findBounds left h leftW).orElse (fun _ => findBounds right h (if w > leftW then w - leftW - 1 else 0))
    | .vsplit top bottom ratio =>
      let topH := (Float.ofNat h * ratio).toUInt64.toNat
      (findBounds top topH w).orElse (fun _ => findBounds bottom (if h > topH then h - topH - 1 else 0) w)
  -- Reserve 1 line for global status/command
  let layoutH := if s.windowHeight > 0 then s.windowHeight - 1 else 0
  (findBounds wg.layout layoutH s.windowWidth).getD (layoutH, s.windowWidth)
def getAllWindowBounds (l : Layout) (h w : Nat) : List (Nat × Nat × Nat × Nat × Nat) :=
  let rec traverse (l : Layout) (r c h w : Nat) (acc : List (Nat × Nat × Nat × Nat × Nat)) : List (Nat × Nat × Nat × Nat × Nat) :=
    match l with
    | .window id _ => (id, r, c, h, w) :: acc
    | .hsplit left right ratio =>
      let leftW := (Float.ofNat w * ratio).toUInt64.toNat
      let acc' := traverse left r c h leftW acc
      traverse right r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0) acc'
    | .vsplit top bottom ratio =>
      let topH := (Float.ofNat h * ratio).toUInt64.toNat
      let acc' := traverse top r c topH w acc
      traverse bottom (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w acc'
  traverse l 0 0 h w []
def getWindowIds (l : Layout) : List Nat :=
  match l with
  | .window id _ => [id]
  | .hsplit left right _ => getWindowIds left ++ getWindowIds right
  | .vsplit top bottom _ => getWindowIds top ++ getWindowIds bottom
end ViE

import ViE.State.Config
import ViE.State.Layout
import ViE.State.Movement
import ViE.Types
import ViE.Buffer.Content
namespace ViE
def EditorState.setMode (s : EditorState) (m : Mode) : EditorState :=
  { s with mode := m }
def EditorState.insertChar (s : EditorState) (c : Char) : EditorState :=
  let cursor := s.getCursor
  let row := cursor.row.val
  let col := cursor.col.val
  let s' := s.updateActiveBuffer fun buffer =>
    modifyLineInBuffer buffer row fun line =>
      let chars := line.toList
      let newChars := (chars.take col) ++ [c] ++ (chars.drop col)
      String.ofList newChars
  s'.setCursor (Point.make row (col + 1))
def EditorState.insertNewline (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  let row := cursor.row.val
  let col := cursor.col.val
  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]
  s'.setCursor (Point.make (row + 1) 0)
def EditorState.deleteBeforeCursor (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  let row := cursor.row.val
  let col := cursor.col.val
  if col > 0 then
    -- Delete char before cursor
    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
    s'.setCursor (Point.make row (col - 1))
  else if row > 0 then
    -- At start of line: join with previous line
    let prevRow := row - 1
    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]
    s'.setCursor (Point.make prevRow newCol)
  else
    s
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
  else
    before ++ after
def EditorState.deleteCurrentLine (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  let s' := s.updateActiveBufferContent fun (buffer : TextBuffer) => deleteLine buffer cursor.row.val
  let newBuffer := s'.activeBufferContent
  let newRow := min cursor.row.val (newBuffer.size.pred)
  let currentLineLen := (getLine newBuffer newRow).map String.length |>.getD 0
  let newCol := min cursor.col.val currentLineLen
  let s'' := s'.setCursor (Point.make newRow newCol)
  { s'' with
    inputState := { s''.inputState with previousKey := none },
    message := "Deleted line"
  }
def EditorState.insertLineBelow (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  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)
def EditorState.insertLineAbove (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  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)
def EditorState.yankCurrentLine (s : EditorState) : EditorState :=
  let cursor := s.getCursor
  let line := getLine s.activeBufferContent cursor.row.val |>.getD ""
  { s with clipboard := some #[stringToLine line], message := "Yanked 1 line" }
def EditorState.pasteBelow (s : EditorState) : EditorState :=
  match s.clipboard with
  | none => { s with message := "Clipboard empty" }
  | some lines =>
    let cursor := s.getCursor
    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)
def EditorState.pasteAbove (s : EditorState) : EditorState :=
  match s.clipboard with
  | none => { s with message := "Clipboard empty" }
  | some lines =>
    let cursor := s.getCursor
    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)
end ViE

import ViE.Types
import ViE.Basic
import ViE.Color
import ViE.Workspace
import ViE.Data.PieceTable
namespace ViE
open ViE.PieceTable
def defaultStatus := (ViE.Color.toBg <|
  (ViE.Color.fromHex "333333").getD
   .brightBlack) ++ (ViE.Color.toFg .white)
def defaultWorkspace : Workspace := {
  rootPath := none
  displayName := "ViE"
}
def defaultConfig : EditorConfig := {
  showLineNumbers := false
  vSplitStr := "│"
  hSplitStr := "─"
  emptyLineMarker := "~"
  statusBarStyle := defaultStatus
  resetStyle := ViE.Color.reset
  fileIcon := "📄 "
  dirIcon := "📁 "
}
def initialInputState : InputState := {
  previousKey := none
  countBuffer := ""
  commandBuffer := ""
  pendingKeys := ""
  lastInputTime := 0
}
def initialBuffer : FileBuffer := {
  id := 0
  filename := none
  dirty := false
  table := PieceTable.fromString ""
  missingEol := false
}
def initialView : ViewState := {
  bufferId := 0
  cursor := Point.zero
  scrollRow := Row.zero
  scrollCol := Col.zero
}
def initialWorkgroupState : WorkgroupState := {
  buffers := [initialBuffer]
  nextBufferId := 1
  layout := .window 0 initialView
  activeWindowId := 0
  nextWindowId := 1
}
def createEmptyWorkgroup (nextBufId : Nat) : WorkgroupState := {
  buffers := [{ initialBuffer with id := nextBufId }]
  nextBufferId := nextBufId + 1
  layout := .window 0 initialView
  activeWindowId := 0
  nextWindowId := 1
}
/-- Helper to create an array of initial workgroup states -/
def makeInitialWorkgroups : Array WorkgroupState :=
  Array.mk (List.replicate 10 initialWorkgroupState)
def initialState : EditorState := {
  mode := .normal
  -- Initialize 10 workgroups
  workgroups := makeInitialWorkgroups
  currentGroup := 0
  message := "Welcome to Lean Editor"
  shouldQuit := false
  config := defaultConfig
  workspace := defaultWorkspace
  clipboard := none
  selectionStart := none
  explorers := []
  inputState := initialInputState
  windowHeight := 0
  windowWidth := 0
  dirty := true
}
end ViE

namespace ViE
inductive Mode where
  | normal
  | insert
  | command
  | visual
  | visualBlock
  deriving Repr, BEq, Inhabited
instance : ToString Mode where
  toString
    | .normal => "NORMAL"
    | .insert => "INSERT"
    | .command => "COMMAND"
    | .visual => "VISUAL"
    | .visualBlock => "VISUAL BLOCK"
end ViE

namespace ViE.Loader
def getUserConfigDir : IO String := do
  let xdgConfig ← IO.getEnv "XDG_CONFIG_HOME"
  match xdgConfig with
  | some dir => return dir ++ "/vie"
  | none =>
    let home ← IO.getEnv "HOME"
    match home with
    | some h => return h ++ "/.config/vie"
    | none => return "./config"
def getCustomBinaryPath : IO String := do
  let dir ← getUserConfigDir
  return dir ++ "/.lake/build/bin/vie"
def buildConfig : IO Bool := do
  let dir ← getUserConfigDir
  try
    let out ← IO.Process.output {
      cmd := "lake"
      args := #["build"]
      cwd := dir
    }
    return out.exitCode == 0
  catch _ =>
    return false
/-- Restart the editor by spawning a new process and waiting for it. -/
def restartEditor (args : List String) : IO Unit := do
  let binPath ← getCustomBinaryPath
  -- Spawn the new process. It will take over the terminal.
  let child ← IO.Process.spawn {
    cmd := binPath
    args := args.toArray
  }
  -- Wait for the new process to finish instead of exiting.
  -- This prevents the shell prompt from flickering or appearing.
  let _ ← child.wait
  IO.Process.exit 0
end ViE.Loader

import ViE.Key.Dispatch
import ViE.Key.Map
import ViE.Key.Input
import ViE.Key.Handler

import ViE.State
import ViE.Types
import ViE.Key.Handler
import ViE.Window.Actions
import ViE.Command.Explorer
import ViE.Command.Dispatch
import ViE.Basic
namespace ViE.Key
open ViE
open ViE.Window
open ViE.Feature
open ViE.Key
/-- Default key bindings. -/
def makeKeyMap (commands : CommandMap) : KeyMap := {
  normal := fun s k => match k with
  | Key.char 'h' =>
      -- Check if in explorer buffer
      let buf := s.getActiveBuffer
      let isExplorer := s.explorers.any (fun (id, _) => id == buf.id)
      if isExplorer then
        -- Navigate to parent directory
        let explorerOpt := s.explorers.find? (fun (id, _) => id == buf.id)
        match explorerOpt with
        | some (_, explorer) =>
          let parentPath := match (System.FilePath.mk explorer.currentPath).parent with
            | some p => p.toString
            | none => "/"
          let s' := { s with inputState := { s.inputState with commandBuffer := s!"ee {parentPath}" } }
          ViE.Command.executeCommand commands s'
        | none => pure $ clearInput (EditorState.moveCursorLeftN s s.getCount)
      else
        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)
  | Key.enter => ViE.Feature.handleExplorerEnter s
  | Key.char 'i' => pure $ s.setMode Mode.insert
  | Key.char 'a' =>
      let s' := EditorState.moveCursorRight s
      pure $ s'.setMode Mode.insert
  | Key.char 'A' =>
      let s' := EditorState.moveToLineEnd s
      pure $ s'.setMode Mode.insert
  | Key.char ':' => pure $ s.setMode Mode.command
  | Key.char 'q' => pure $ s.setMode Mode.command
  | Key.char 'o' => pure $ (EditorState.insertLineBelow s).setMode Mode.insert
  | Key.char 'O' => pure $ (EditorState.insertLineAbove s).setMode Mode.insert
  | Key.char 'v' => pure $ EditorState.startVisualMode s
  | Key.char 'V' => pure $ EditorState.startVisualBlockMode s
  | Key.char '0' =>
     if s.inputState.countBuffer.isEmpty then pure $ clearInput (EditorState.moveToLineStart s)
     else
        pure { s with inputState := { s.inputState with countBuffer := s.inputState.countBuffer.push '0' } }
  | Key.char '$' => pure $ clearInput (EditorState.moveToLineEnd s)
  | Key.char 'p' => pure $ clearInput (EditorState.pasteBelow s)
  | Key.char 'P' => pure $ clearInput (EditorState.pasteAbove s)
  | Key.char 'y' =>
     match s.inputState.previousKey with
     | some 'y' => pure $ clearInput (EditorState.yankCurrentLine s)
     | _ => pure { s with inputState := { s.inputState with previousKey := some 'y' } }
  | Key.char '|' =>
    let n := s.getCount
    pure $ clearInput (EditorState.jumpToColumn s n)
  | Key.char 'd' =>
    match s.inputState.previousKey with
    | some 'd' => pure $ s.deleteCurrentLine
    | _ => pure { s with inputState := { s.inputState with previousKey := some 'd' } }
  | Key.ctrl 'w' =>
      pure { s with inputState := { s.inputState with previousKey := some '\x17' } }
  | Key.char c =>
      if s.inputState.previousKey == some '\x17' then
         -- Handle window command
         let s' := { s with inputState := { s.inputState with previousKey := none } }
         match c with
         | 'h' => pure $ switchWindow s' .left
         | 'j' => pure $ switchWindow s' .down
         | 'k' => pure $ switchWindow s' .up
         | 'l' => pure $ switchWindow s' .right
         | 's' => pure $ splitWindow s' true
         | 'v' => pure $ splitWindow s' false
         | 'q' => pure $ closeActiveWindow s'
         | 'w' => pure $ cycleWindow s'
         | 'c' => pure $ cycleWindow s'
         | _ => pure s'
      else if s.inputState.previousKey == some 'g' then
         -- Handle g commands
         let s' := { s with inputState := { s.inputState with previousKey := none } }
         match c with
         | 't' =>
            let next := (s.currentGroup + 1) % 10
            let s'' := s.switchToWorkgroup next
            pure { s'' with message := s!"Switched to workgroup {next}" }
         | 'T' =>
            let prev := if s.currentGroup == 0 then 9 else s.currentGroup - 1
            let s'' := s.switchToWorkgroup prev
            pure { s'' with message := s!"Switched to workgroup {prev}" }
         | _ => pure s'
      else
         match c with
         | 'g' =>
            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' } }
         | 'G' =>
            let line := match s.inputState.countBuffer.toNat? with
              | some n => n
              | none => s.getActiveBuffer.lineCount
            pure $ clearInput (EditorState.jumpToLine s line)
         | _ =>
            if c.isDigit then
               pure { s with inputState := { s.inputState with countBuffer := s.inputState.countBuffer.push c } }
            else
               pure { s with inputState := { s.inputState with countBuffer := "", previousKey := none } }
  | Key.alt c =>
      let s' := { s with inputState := { s.inputState with previousKey := none } }
      match c with
      | 'h' => pure $ switchWindow s' .left
      | 'j' => pure $ switchWindow s' .down
      | 'k' => pure $ switchWindow s' .up
      | 'l' => pure $ switchWindow s' .right
      | 'H' => pure $ resizeWindow s' .left 0.05
      | 'J' => pure $ resizeWindow s' .down 0.05
      | 'K' => pure $ resizeWindow s' .up 0.05
      | 'L' => pure $ resizeWindow s' .right 0.05
      | _ => pure s'
  | _ => pure { s with inputState := { s.inputState with countBuffer := "", previousKey := none } },
  insert := fun s k => match k with
    | Key.esc => pure $ s.setMode Mode.normal
    | Key.backspace => pure $ s.deleteBeforeCursor
    | Key.char c => pure $ s.insertChar c
    | Key.enter => pure s.insertNewline
    | _ => pure s,
  command := handleCommandInput commands,
  visual := fun s k => match k with
    | Key.esc => pure $ EditorState.exitVisualMode s
    | Key.char 'v' => pure $ EditorState.exitVisualMode s
    | Key.char 'h' => 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)
    | Key.char '0' => pure $ clearInput (EditorState.moveToLineStart s)
    | Key.char '$' => pure $ clearInput (EditorState.moveToLineEnd s)
    | Key.char 'G' =>
        let line := match s.inputState.countBuffer.toNat? with
          | some n => n
          | none => s.getActiveBuffer.lineCount
        pure $ clearInput (EditorState.jumpToLine s line)
    | Key.char 'd' => pure $ EditorState.deleteSelection s
    | Key.char 'x' => pure $ EditorState.deleteSelection s
    | Key.char 'y' => pure $ EditorState.yankSelection s
    | Key.char c =>
         match c with
         | 'g' =>
            match s.inputState.previousKey with
            | some 'g' =>
               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' } }
         | _ =>
            if c.isDigit then
               pure { s with inputState := { s.inputState with countBuffer := s.inputState.countBuffer.push c } }
            else
               pure s
    | _ => pure s,
  visualBlock := fun s k => match k with
    | Key.esc => pure $ EditorState.exitVisualMode s
    | Key.char 'v' => pure $ EditorState.exitVisualMode s
    | Key.char 'V' => pure $ EditorState.exitVisualMode s
    | Key.char 'h' => 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)
    | Key.char '0' => pure $ clearInput (EditorState.moveToLineStart s)
    | Key.char '$' => pure $ clearInput (EditorState.moveToLineEnd s)
    | Key.char 'G' =>
        let line := match s.inputState.countBuffer.toNat? with
          | some n => n
          | none => s.getActiveBuffer.lineCount
        pure $ clearInput (EditorState.jumpToLine s line)
    | Key.char 'd' => pure $ EditorState.deleteSelection s
    | Key.char 'x' => pure $ EditorState.deleteSelection s
    | Key.char 'y' => pure $ EditorState.yankSelection s
    | Key.char c =>
         match c with
         | 'g' =>
            match s.inputState.previousKey with
            | some 'g' =>
               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' } }
         | _ =>
            if c.isDigit then
               pure { s with inputState := { s.inputState with countBuffer := s.inputState.countBuffer.push c } }
            else
               pure s
    | _ => pure s
}
end ViE.Key

import ViE.State
import ViE.Types
namespace ViE.Key
/-- Parse a character into a list of keys, handling escape sequences statefully. -/
def parseKey (state : EditorState) (c : Char) (currentTime : Nat) : (EditorState × List Key) :=
  -- If we have pending keys (escape sequence in progress)
  if state.inputState.pendingKeys.length > 0 then
    let pending := state.inputState.pendingKeys.push c
    -- Check for known sequences
    match pending with
    | "\x1b" =>
      ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])
    | "\x1b[" =>
       -- CSI sequence starter, keep waiting
       ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])
    | "\x1b[A" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.up])
    | "\x1b[B" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.down])
    | "\x1b[C" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.right])
    | "\x1b[D" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.left])
    | "\x1b[H" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.unknown 'H']) -- Home?
    | "\x1b[F" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.unknown 'F']) -- End?
    | _ =>
       -- Unknown sequence or incomplete?
       -- If length is long enough (e.g. 3 chars) and no match, flush as individual keys?
       -- Or check if it starts with valid prefix.
       if pending.startsWith "\x1b[" && pending.length < 5 then
          ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])
       else
          -- Flush everything as individual characters
          -- (Note: this simplifies, strictly we should map char-by-char)
          let keys := pending.toList.map (fun x => if x == '\x1b' then Key.esc else Key.char x)
          ({ state with inputState := { state.inputState with pendingKeys := "" } }, keys)
  else
    -- No pending keys
    if c == '\x1b' then
       -- Start escape sequence
       ({ state with inputState := { state.inputState with pendingKeys := "\x1b", lastInputTime := currentTime } }, [])
    else
       -- Normal character (using logic similar to old fromChar)
       let k := match c with
        | '\x01' => Key.ctrl 'a'
        | '\x02' => Key.ctrl 'b'
        | '\x03' => Key.ctrl 'c'
        | '\x04' => Key.ctrl 'd'
        | '\x05' => Key.ctrl 'e'
        | '\x06' => Key.ctrl 'f'
        | '\x07' => Key.ctrl 'g'
        | '\x08' => Key.ctrl 'h'
        | '\x09' => Key.ctrl 'i'
        | '\x0b' => Key.ctrl 'k'
        | '\x0c' => Key.ctrl 'l'
        | '\x0e' => Key.ctrl 'n'
        | '\x0f' => Key.ctrl 'o'
        | '\x10' => Key.ctrl 'p'
        | '\x11' => Key.ctrl 'q'
        | '\x12' => Key.ctrl 'r'
        | '\x13' => Key.ctrl 's'
        | '\x14' => Key.ctrl 't'
        | '\x15' => Key.ctrl 'u'
        | '\x16' => Key.ctrl 'v'
        | '\x17' => Key.ctrl 'w'
        | '\x18' => Key.ctrl 'x'
        | '\x19' => Key.ctrl 'y'
        | '\x1a' => Key.ctrl 'z'
        | '\x7f' => Key.backspace
        | '\x0a' | '\x0d' => Key.enter
        | _ => Key.char c
       (state, [k])
/-- Check for escape sequence timeout. -/
def checkTimeout (state : EditorState) (currentTime : Nat) : (EditorState × List Key) :=
  if state.inputState.pendingKeys.length > 0 then
    if currentTime - state.inputState.lastInputTime > 50 then -- 50ms timeout
       -- Timeout! Flush pending keys as is.
       let keys := state.inputState.pendingKeys.toList.map (fun x => if x == '\x1b' then Key.esc else Key.char x)
       ({ state with inputState := { state.inputState with pendingKeys := "" } }, keys)
    else
       (state, [])
  else
    (state, [])
end ViE.Key

import ViE.State
import ViE.Types
import ViE.Command.Dispatch
namespace ViE.Key
open ViE
def handleCommandInput (commands : CommandMap) (state : EditorState) (k : Key) : IO EditorState := do
  match k with
  | Key.esc => return { state with mode := .normal, message := "", inputState := { state.inputState with commandBuffer := "" } }
  | Key.enter =>
    let newState ← ViE.Command.executeCommand commands state
    if newState.shouldQuit then
      return newState
    else
      return { newState with mode := .normal, inputState := { newState.inputState with commandBuffer := "" } }
  | Key.backspace =>
    if state.inputState.commandBuffer.length > 0 then
      let newCmd := state.inputState.commandBuffer.dropEnd 1
      return { state with inputState := { state.inputState with commandBuffer := newCmd.toString } }
    else
      return state
  | Key.char c => return { state with inputState := { state.inputState with commandBuffer := state.inputState.commandBuffer.push c } }
  | _ => return state
def clearInput (s : EditorState) : EditorState :=
  { s with inputState := { s.inputState with countBuffer := "", previousKey := none } }
end ViE.Key

import ViE.State
import ViE.Types
import ViE.Window.Actions
import ViE.Key.Map
namespace ViE.Key
open ViE
def update (config : Config) (state : EditorState) (k : Key) : IO EditorState := do
  let newState ← match state.mode with
  | .normal => config.bindings.normal state k
  | .insert => config.bindings.insert state k
  | .command => config.bindings.command state k
  | .visual => config.bindings.visual state k
  | .visualBlock => config.bindings.visualBlock state k
  return ViE.Window.enforceScroll newState
end ViE.Key

import ViE.State
import ViE.Basic
import ViE.Buffer.LowIO
namespace ViE
open ViE.PieceTable
/-- Save buffer to file with error handling using atomic write. -/
def saveBuffer (state : EditorState) (filename : String) : IO EditorState := do
  let tempFilename := filename ++ ".tmp"
  try
    let buffer := state.getActiveBuffer
    -- Get content from PieceTable
    let content := PieceTable.toString buffer.table
    -- Ensure POSIX compliance (end with newline)
    -- If missingEol is true, we preserve the "no newline at EOF" state (unless user added one).
    -- If missingEol is false, we enforce a trailing newline.
    let finalContent :=
      if buffer.missingEol then
        content
      else
        if !content.isEmpty && content.back != '\n' then
          content ++ "\n"
        else
          content
    -- Write to temporary file first
    IO.FS.writeFile tempFilename finalContent
    -- Rename temp file to target file (atomic on POSIX)
    IO.FS.rename tempFilename filename
    -- After save, reload as clean mmap
    let newBuffer ← loadBufferByteArray filename
    let newBuffer := { newBuffer with id := buffer.id, dirty := false }
    -- Update the buffer in the current workgroup
    let state' := state.updateActiveBuffer fun _ => newBuffer
    return { state' with message := s!"\"{filename}\" saved" }
  catch e =>
    -- Try to clean up temp file if it exists (ignoring errors)
    try
      IO.FS.removeFile tempFilename
    catch _ => pure ()
    -- Keep dirty flag on error to prevent data loss
    return { state with message := s!"Error saving \"{filename}\": {e}" }
end ViE

import ViE.Data.PieceTable.Piece
import ViE.Data.PieceTable.Types
import ViE.Data.PieceTable.Tree
namespace ViE.PieceTable
/-- Chunk size for splitting large files (16KB) -/
def PieceTable.ChunkSize : Nat := 1024 * 16
/-- Construct from bytes -/
def PieceTable.fromByteArray (bytes : ByteArray) : PieceTable :=
  if bytes.size == 0 then
    { original := bytes, add := ByteArray.empty, tree := PieceTree.empty }
  else
    -- Split bytes into chunks to avoid monolithic pieces
    let totalSize := bytes.size
    let rec splitChunks (start : Nat) (acc : Array Piece) : Array Piece :=
      if start >= totalSize then acc
      else
        let len := min PieceTable.ChunkSize (totalSize - start)
        let lines := ViE.Unicode.countNewlines bytes start len
        let chars := ViE.Unicode.countChars bytes start len
        let piece := { source := .original, start := start, length := len, lineBreaks := lines, charCount := chars }
        splitChunks (start + len) (acc.push piece)
    termination_by totalSize - start
    decreasing_by
      simp_wf
      rw [Nat.sub_add_eq]
      have h : start < totalSize := Nat.lt_of_not_le (by assumption)
      apply Nat.sub_lt_self
      · have h1 : 0 < totalSize - start := Nat.sub_pos_of_lt h
        apply Nat.lt_min.mpr
        constructor
        . show 0 < PieceTable.ChunkSize
          unfold PieceTable.ChunkSize
          exact Nat.zero_lt_succ _
        · assumption
      · apply Nat.min_le_right
    let pieces := splitChunks 0 #[]
    let tree := PieceTree.fromPieces pieces
    { original := bytes, add := ByteArray.empty, tree := tree }
/-- Construct from initial string -/
def PieceTable.fromString (s : String) : PieceTable :=
  PieceTable.fromByteArray s.toUTF8
/-- Convert tree to string -/
def PieceTable.toString (pt : PieceTable) : String :=
  PieceTree.getSubstring pt.tree 0 pt.tree.length pt
/-- Insert text at offset -/
def PieceTable.insert (pt : PieceTable) (offset : Nat) (text : String) : PieceTable :=
  if text.isEmpty then pt
  else
    let (pt', newPiece) := PieceTableHelper.appendText pt text
    let (l, r) := PieceTree.split pt.tree offset pt'
    let mid := PieceTree.mkLeaf #[newPiece]
    let newTree := PieceTree.concat (PieceTree.concat l mid) r
    { pt' with tree := newTree }
/-- Delete range [offset, offset + length) -/
def PieceTable.delete (pt : PieceTable) (offset : Nat) (length : Nat) : PieceTable :=
  if length == 0 then pt
  else
    let newTree := PieceTree.delete pt.tree offset length pt
    { pt with tree := newTree }
/-- Get line from buffer -/
def PieceTable.getLine (pt : PieceTable) (lineIdx : Nat) : Option String :=
  PieceTree.getLine pt.tree lineIdx pt
/-- Get line range from buffer -/
def PieceTable.getLineRange (pt : PieceTable) (lineIdx : Nat) : Option (Nat × Nat) :=
  PieceTree.getLineRange pt.tree lineIdx pt
/-- Get line char length from buffer -/
def PieceTable.getLineLength (pt : PieceTable) (lineIdx : Nat) : Option Nat :=
  PieceTree.getLineLength pt.tree lineIdx pt
end ViE.PieceTable

import ViE.Data.PieceTable.Piece
namespace ViE.PieceTable
/-- A node in the B+ Piece Tree -/
inductive PieceTree where
  | empty
  | leaf (pieces : Array Piece) (stats : Stats)
  | internal (children : Array PieceTree) (stats : Stats)
  deriving Repr, Inhabited
structure PieceTable where
  original : ByteArray
  add : ByteArray
  tree : PieceTree
  deriving Inhabited
end ViE.PieceTable

import ViE.Data.PieceTable.Piece
import ViE.Data.PieceTable.Types
import ViE.Unicode
namespace ViE.PieceTable
namespace PieceTableHelper
/-- Get the buffer data corresponding to a source -/
def getBuffer (pt : PieceTable) (source : BufferSource) : ByteArray :=
  match source with
  | .original => pt.original
  | .add => pt.add
/-- Append text to add buffer -/
def appendText (pt : PieceTable) (text : String) : (PieceTable × Piece) :=
  let bytes := text.toUTF8
  let start := pt.add.size
  let len := bytes.size
  let newAdd := pt.add ++ bytes
  let newLines := ViE.Unicode.countNewlines bytes 0 len
  let newChars := ViE.Unicode.countChars bytes 0 len
  let piece := { source := .add, start := start, length := len, lineBreaks := newLines, charCount := newChars }
  ({ pt with add := newAdd }, piece)
/-- Split a piece into two at a given relative offset. -/
def splitPiece (pt : PieceTable) (p : Piece) (offset : Nat) : (Piece × Piece) :=
  let buf := getBuffer pt p.source
  let leftLen := offset
  let rightLen := p.length - offset
  let leftLines := ViE.Unicode.countNewlines buf p.start leftLen
  let rightLines := p.lineBreaks - leftLines
  let leftChars := ViE.Unicode.countChars buf p.start leftLen
  let rightChars := p.charCount - leftChars
  let leftP := { p with length := leftLen, lineBreaks := leftLines, charCount := leftChars }
  let rightP := { p with start := p.start + leftLen, length := rightLen, lineBreaks := rightLines, charCount := rightChars }
  (leftP, rightP)
end PieceTableHelper
namespace PieceTree
/-- Get stats of a tree -/
def stats : PieceTree → Stats
  | empty => Stats.empty
  | leaf _ s => s
  | internal _ s => s
def length (t : PieceTree) : Nat := t.stats.bytes
def lineBreaks (t : PieceTree) : Nat := t.stats.lines
def height (t : PieceTree) : Nat := t.stats.height
/-- Helper to construct a leaf node from pieces -/
def mkLeaf (pieces : Array Piece) : PieceTree :=
  let stats := pieces.foldl (fun s p =>
    { s with bytes := s.bytes + p.length, lines := s.lines + p.lineBreaks, chars := s.chars + p.charCount })
    { bytes := 0, lines := 0, chars := 0, height := 1 }
  leaf pieces stats
/-- Helper to construct an internal node from children -/
def mkInternal (children : Array PieceTree) : PieceTree :=
  if children.isEmpty then empty
  else
    let firstHeight := (children[0]!).height
    let h := firstHeight + 1
    let stats := children.foldl (fun s c =>
      let cs := c.stats
      { s with bytes := s.bytes + cs.bytes, lines := s.lines + cs.lines, chars := s.chars + cs.chars })
      { bytes := 0, lines := 0, chars := 0, height := h }
    internal children stats
/-- Concatenate two trees -/
partial def concat (l : PieceTree) (r : PieceTree) : PieceTree :=
  match l, r with
  | empty, _ => r
  | _, empty => l
  | leaf ps1 _, leaf ps2 _ =>
    let ps := ps1 ++ ps2
    if ps.size <= NodeCapacity then
      mkLeaf ps
    else
      -- Split into two leaves
      let mid := ps.size / 2
      let l := mkLeaf (ps.extract 0 mid)
      let r := mkLeaf (ps.extract mid ps.size)
      mkInternal #[l, r]
  | internal cs1 _, internal cs2 _ =>
    if l.height == r.height then
      let cs := cs1 ++ cs2
      if cs.size <= NodeCapacity then
        mkInternal cs
      else
        let mid := cs.size / 2
        let l := mkInternal (cs.extract 0 mid)
        let r := mkInternal (cs.extract mid cs.size)
        mkInternal #[l, r]
    else if l.height > r.height then
      -- Append r to the last child of l
      let lastIdx := cs1.size - 1
      let lastChild := cs1[lastIdx]!
      let newLast := concat lastChild r
      if newLast.height == lastChild.height then
        mkInternal (cs1.set! lastIdx newLast)
      else
        match newLast with
        | internal subChildren _ =>
             let newCs := cs1.pop ++ subChildren
             if newCs.size <= NodeCapacity then mkInternal newCs
             else
                let mid := newCs.size / 2
                mkInternal #[mkInternal (newCs.extract 0 mid), mkInternal (newCs.extract mid newCs.size)]
        | _ => mkInternal (cs1.push newLast)
    else -- l.height < r.height
      let firstChild := cs2[0]!
      let newFirst := concat l firstChild
      if newFirst.height == firstChild.height then
        mkInternal (cs2.set! 0 newFirst)
      else
         match newFirst with
         | internal subChildren _ =>
             let newCs := subChildren ++ cs2.extract 1 cs2.size
             if newCs.size <= NodeCapacity then mkInternal newCs
             else
                let mid := newCs.size / 2
                mkInternal #[mkInternal (newCs.extract 0 mid), mkInternal (newCs.extract mid newCs.size)]
         | _ => mkInternal ((#[newFirst] ++ cs2))
  | leaf _ _, internal _ _ =>
      let firstChild := match r with | internal cs _ => cs[0]! | _ => empty
      let newFirst := concat l firstChild
      match r with
      | internal cs2 _ =>
          if newFirst.height == firstChild.height then
            mkInternal (cs2.set! 0 newFirst)
          else
             match newFirst with
             | internal subChildren _ =>
                 let newCs := subChildren ++ cs2.extract 1 cs2.size
                 if newCs.size <= NodeCapacity then mkInternal newCs
                 else
                    let mid := newCs.size / 2
                    mkInternal #[mkInternal (newCs.extract 0 mid), mkInternal (newCs.extract mid newCs.size)]
             | _ => mkInternal ((#[newFirst] ++ cs2))
      | _ => empty
  | internal _ _, leaf _ _ =>
      let cs1 := match l with | internal cs _ => cs | _ => #[]
      let lastIdx := cs1.size - 1
      let lastChild := cs1[lastIdx]!
      let newLast := concat lastChild r
      if newLast.height == lastChild.height then
        mkInternal (cs1.set! lastIdx newLast)
      else
        match newLast with
        | internal subChildren _ =>
            let newCs := cs1.pop ++ subChildren
            if newCs.size <= NodeCapacity then mkInternal newCs
            else
               let mid := newCs.size / 2
               mkInternal #[mkInternal (newCs.extract 0 mid), mkInternal (newCs.extract mid newCs.size)]
        | _ => mkInternal (cs1.push newLast)
/-- Split a leaf node at a specific piece index and internal offset -/
def splitLeaf (pieces : Array Piece) (stats : Stats) (pt : PieceTable) (offset : Nat) : (PieceTree × PieceTree) :=
  let rec findPiece (i : Nat) (currentOff : Nat) : (Nat × Nat) :=
    if i >= pieces.size then (pieces.size, currentOff)
    else
      let p := pieces[i]!
      if currentOff + p.length > offset then (i, currentOff)
      else findPiece (i + 1) (currentOff + p.length)
  let (idx, pStart) := findPiece 0 0
  if idx >= pieces.size then
    (leaf pieces stats, empty)
  else
    let p := pieces[idx]!
    let splitOff := offset - pStart
    if splitOff == 0 then
      let leftArr := pieces.extract 0 idx
      let rightArr := pieces.extract idx pieces.size
      (mkLeaf leftArr, mkLeaf rightArr)
    else if splitOff == p.length then
      let leftArr := pieces.extract 0 (idx + 1)
      let rightArr := pieces.extract (idx + 1) pieces.size
      (mkLeaf leftArr, mkLeaf rightArr)
    else
      let (p1, p2) := PieceTableHelper.splitPiece pt p splitOff
      let leftPieces := (pieces.extract 0 idx).push p1
      let rightPieces := (#[p2]).append (pieces.extract (idx + 1) pieces.size)
      (mkLeaf leftPieces, mkLeaf rightPieces)
/-- Split the tree at a given character offset. -/
partial def split (t : PieceTree) (offset : Nat) (pt : PieceTable) : (PieceTree × PieceTree) :=
  match t with
  | empty => (empty, empty)
  | leaf pieces s => splitLeaf pieces s pt offset
  | internal children curStats =>
    if offset == 0 then (empty, t)
    else if offset >= curStats.bytes then (t, empty)
    else
      let rec scan (i : Nat) (accOff : Nat) : (PieceTree × PieceTree) :=
        if i >= children.size then (t, empty)
        else
          let c := children[i]!
          if accOff + c.length > offset then
            let (cLeft, cRight) := split c (offset - accOff) pt
            let leftChildren := (children.extract 0 i).push cLeft
            let rightChildren := (#[cRight]).append (children.extract (i + 1) children.size)
            let leftFiltered := leftChildren.filter (fun c => c.length > 0)
            let rightFiltered := rightChildren.filter (fun c => c.length > 0)
            (mkInternal leftFiltered, mkInternal rightFiltered)
          else
            scan (i + 1) (accOff + c.length)
      scan 0 0
/-- Delete range [offset, offset + length) -/
def delete (t : PieceTree) (offset : Nat) (length : Nat) (pt : PieceTable) : PieceTree :=
  if length == 0 then t
  else
    let (l, r) := split t offset pt
    let (_, r') := split r length pt
    concat l r'
/-- Find offset of the N-th newline (0-indexed). -/
partial def findNthNewline (t : PieceTree) (n : Nat) (pt : PieceTable) : Nat :=
  match t with
  | empty => 0
  | leaf pieces _ =>
    let rec scanPieces (i : Nat) (remainingN : Nat) (accOffset : Nat) : Nat :=
      if i >= pieces.size then accOffset
      else
        let p := pieces[i]!
        if remainingN < p.lineBreaks then
          let buf := PieceTableHelper.getBuffer pt p.source
          let rec scan (j : Nat) (cnt : Nat) : Nat :=
            if j >= p.length then j
            else
              if buf[p.start + j]! == 10 then
                if cnt == remainingN then j
                else scan (j + 1) (cnt + 1)
              else scan (j + 1) cnt
          accOffset + (scan 0 0)
        else
          scanPieces (i + 1) (remainingN - p.lineBreaks) (accOffset + p.length)
    scanPieces 0 n 0
  | internal children _ =>
    let rec scanChildren (i : Nat) (remainingN : Nat) (accOffset : Nat) : Nat :=
      if i >= children.size then accOffset
      else
        let child := children[i]!
        let childLines := child.lineBreaks
        if remainingN < childLines then
          accOffset + findNthNewline child remainingN pt
        else
          scanChildren (i + 1) (remainingN - childLines) (accOffset + child.length)
    scanChildren 0 n 0
/-- Get substring of tree from start to end offset -/
partial def getSubstring (t : PieceTree) (startOff endOff : Nat) (pt : PieceTable) : String :=
  if startOff >= endOff then ""
  else
    let rec traverse (t : PieceTree) (currentOff : Nat) : String :=
      let tLen := t.length
      if currentOff + tLen <= startOff || currentOff >= endOff then ""
      else
        match t with
        | empty => ""
        | leaf pieces _ =>
           let rec scan (i : Nat) (off : Nat) (acc : String) : String :=
             if i >= pieces.size then acc
             else
               let p := pieces[i]!
               let pStart := off
               let pEnd := off + p.length
               let readStart := max startOff pStart
               let readEnd := min endOff pEnd
               if readStart < readEnd then
                 let buf := PieceTableHelper.getBuffer pt p.source
                 let sliceStart := p.start + (readStart - pStart)
                 let sliceEnd := p.start + (readEnd - pStart)
                 let str := String.fromUTF8! (buf.extract sliceStart sliceEnd)
                 scan (i + 1) pEnd (acc ++ str)
               else
                 scan (i + 1) pEnd acc
           scan 0 currentOff ""
        | internal children _ =>
           let rec scanInternal (i : Nat) (off : Nat) (acc : String) : String :=
             if i >= children.size then acc
             else
               let c := children[i]!
               let s := traverse c off
               scanInternal (i + 1) (off + c.length) (acc ++ s)
           scanInternal 0 currentOff ""
    traverse t 0
/-- Get total string length of a range (counting chars, not bytes, without allocation) -/
partial def countCharsInRange (t : PieceTree) (startOff endOff : Nat) (pt : PieceTable) : Nat :=
  if startOff >= endOff then 0
  else
    let rec traverse (t : PieceTree) (currentOff : Nat) : Nat :=
      let tLen := t.length
      if currentOff + tLen <= startOff || currentOff >= endOff then 0
      else if currentOff >= startOff && currentOff + tLen <= endOff then
        t.stats.chars
      else
        match t with
        | empty => 0
        | leaf pieces _ =>
           let rec scan (i : Nat) (off : Nat) (acc : Nat) : Nat :=
             if i >= pieces.size then acc
             else
               let p := pieces[i]!
               let pStart := off
               let pEnd := off + p.length
               if pEnd <= startOff || pStart >= endOff then
                 scan (i + 1) pEnd acc
               else if pStart >= startOff && pEnd <= endOff then
                 scan (i + 1) pEnd (acc + p.charCount)
               else
                 let readStart := max startOff pStart
                 let readEnd := min endOff pEnd
                 let buf := PieceTableHelper.getBuffer pt p.source
                 let sliceStart := p.start + (readStart - pStart)
                 let sliceLen := readEnd - readStart
                 let cnt := ViE.Unicode.countChars buf sliceStart sliceLen
                 scan (i + 1) pEnd (acc + cnt)
           scan 0 currentOff 0
        | internal children _ =>
           let rec scanInternal (i : Nat) (off : Nat) (acc : Nat) : Nat :=
             if i >= children.size then acc
             else
               let c := children[i]!
               let s := traverse c off
               scanInternal (i + 1) (off + c.length) (acc + s)
           scanInternal 0 currentOff 0
    traverse t 0
/-- Get line char length (0-indexed). Excludes newline at end of line. -/
def getLineLength (t : PieceTree) (lineIdx : Nat) (pt : PieceTable) : Option Nat :=
  let totalLines := t.lineBreaks
  if lineIdx > totalLines then none
  else
    let startOffset := if lineIdx == 0 then 0 else findNthNewline t (lineIdx - 1) pt + 1
    let endOffset :=
      if lineIdx == totalLines then
        t.length
      else
        findNthNewline t lineIdx pt
    some (countCharsInRange t startOffset endOffset pt)
def getLine (t : PieceTree) (lineIdx : Nat) (pt : PieceTable) : Option String :=
  let totalLines := t.lineBreaks
  if lineIdx > totalLines then none
  else
    let startOffset := if lineIdx == 0 then 0 else findNthNewline t (lineIdx - 1) pt + 1
    let endOffset :=
      if lineIdx == totalLines then
        t.length
      else
        findNthNewline t lineIdx pt
    some (getSubstring t startOffset endOffset pt)
/-- Get line range (start, length) -/
def getLineRange (t : PieceTree) (lineIdx : Nat) (pt : PieceTable) : Option (Nat × Nat) :=
  let totalLines := t.lineBreaks
  if lineIdx > totalLines then none
  else
    let startOffset := if lineIdx == 0 then 0 else findNthNewline t (lineIdx - 1) pt + 1
    let endOffset :=
      if lineIdx == totalLines then
        t.length
      else
        findNthNewline t lineIdx pt
    some (startOffset, endOffset - startOffset)
/-- Build a tree from a list of pieces (Bottom-Up construction) -/
partial def fromPieces (pieces : Array Piece) : PieceTree :=
  if pieces.isEmpty then empty
  else
    -- Step 1: Create Leaves
    let rec mkLeaves (i : Nat) (acc : Array PieceTree) : Array PieceTree :=
      if i >= pieces.size then acc
      else
        let chunk := pieces.extract i (i + NodeCapacity)
        let leaf := mkLeaf chunk
        mkLeaves (i + NodeCapacity) (acc.push leaf)
    let leaves := mkLeaves 0 #[]
    -- Step 2: Build Internal Nodes recursively
    let rec buildLevel (nodes : Array PieceTree) : PieceTree :=
      if nodes.size == 1 then
        nodes[0]!
      else
        let rec mkNextLevel (i : Nat) (acc : Array PieceTree) : Array PieceTree :=
          if i >= nodes.size then acc
          else
            let chunk := nodes.extract i (i + NodeCapacity)
            let node := mkInternal chunk
            mkNextLevel (i + NodeCapacity) (acc.push node)
        buildLevel (mkNextLevel 0 #[])
    buildLevel leaves
end PieceTree
end ViE.PieceTable

namespace ViE.PieceTable
/-- Source of a piece: either the original file (read-only) or the add buffer (append-only) -/
inductive BufferSource where
  | original
  | add
  deriving Repr, BEq, Inhabited
/-- A piece descriptor pointing to a range in a source buffer -/
structure Piece where
  source : BufferSource
  start : Nat
  length : Nat
  lineBreaks : Nat
  charCount : Nat
  deriving Repr, BEq, Inhabited
/-- Aggregated statistics for a node -/
structure Stats where
  bytes : Nat
  lines : Nat
  chars : Nat
  height : Nat
  deriving Repr, Inhabited, BEq
def Stats.empty : Stats := { bytes := 0, lines := 0, chars := 0, height := 0 }
def Stats.ofPiece (p : Piece) : Stats :=
  { bytes := p.length, lines := p.lineBreaks, chars := p.charCount, height := 1 }
instance : Add Stats where
  add a b := {
    bytes := a.bytes + b.bytes,
    lines := a.lines + b.lines,
    chars := a.chars + b.chars,
    height := max a.height b.height
  }
/-- B+ Tree Node Capacity (Branching Factor) -/
def NodeCapacity : Nat := 32
end ViE.PieceTable

namespace ViE
/-- Source of a piece: either the original file (read-only) or the add buffer (append-only) -/
inductive BufferSource where
  | original
  | add
  deriving Repr, BEq, Inhabited
/-- A piece descriptor pointing to a range in a source buffer -/
structure Piece where
  source : BufferSource
  start : Nat
  length : Nat
  lineBreaks : Nat
  charCount : Nat
  deriving Repr, BEq, Inhabited
/-- Aggregated statistics for a node -/
structure Stats where
  bytes : Nat
  lines : Nat
  chars : Nat
  height : Nat
  deriving Repr, Inhabited, BEq
def Stats.empty : Stats := { bytes := 0, lines := 0, chars := 0, height := 0 }
def Stats.ofPiece (p : Piece) : Stats :=
  { bytes := p.length, lines := p.lineBreaks, chars := p.charCount, height := 1 }
instance : Add Stats where
  add a b := {
    bytes := a.bytes + b.bytes,
    lines := a.lines + b.lines,
    chars := a.chars + b.chars,
    height := max a.height b.height
  }
/-- B+ Tree Node Capacity (Branching Factor) -/
def NodeCapacity : Nat := 32
end ViE

import ViE.State
namespace ViE
/-- Parse a character into a list of keys, handling escape sequences statefully. -/
def parseKey (state : EditorState) (c : Char) (currentTime : Nat) : (EditorState × List Key) :=
  -- If we have pending keys (escape sequence in progress)
  if state.inputState.pendingKeys.length > 0 then
    let pending := state.inputState.pendingKeys.push c
    -- Check for known sequences
    match pending with
    | "\x1b" =>
       -- 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.
       ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])
    | "\x1b[" =>
       -- CSI sequence starter, keep waiting
       ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])
    | "\x1b[A" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.up])
    | "\x1b[B" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.down])
    | "\x1b[C" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.right])
    | "\x1b[D" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.left])
    | "\x1b[H" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.unknown 'H']) -- Home?
    | "\x1b[F" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.unknown 'F']) -- End?
    | _ =>
       -- Check for Alt+Char: Escape followed by a single char
       if pending.length == 2 && pending.startsWith "\x1b" then
          match pending.toList with
          | [_, c] => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.alt c])
          | _ => -- Should be impossible given length check
             let keys := pending.toList.map (fun x => if x == '\x1b' then Key.esc else Key.char x)
             ({ state with inputState := { state.inputState with pendingKeys := "" } }, keys)
       -- Check if it looks like a CSI sequence
       else if pending.startsWith "\x1b[" && pending.length < 5 then
          ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])
       else
          -- Flush everything as individual characters
          let keys := pending.toList.map (fun x => if x == '\x1b' then Key.esc else Key.char x)
          ({ state with inputState := { state.inputState with pendingKeys := "" } }, keys)
  else
    -- No pending keys
    if c == '\x1b' then
       -- Start escape sequence
       ({ state with inputState := { state.inputState with pendingKeys := "\x1b", lastInputTime := currentTime } }, [])
    else
       -- Normal character (using logic similar to old fromChar)
       let k := match c with
        | '\x01' => Key.ctrl 'a'
        | '\x02' => Key.ctrl 'b'
        | '\x03' => Key.ctrl 'c'
        | '\x04' => Key.ctrl 'd'
        | '\x05' => Key.ctrl 'e'
        | '\x06' => Key.ctrl 'f'
        | '\x07' => Key.ctrl 'g'
        | '\x08' => Key.ctrl 'h'
        | '\x09' => Key.ctrl 'i'
        | '\x0b' => Key.ctrl 'k'
        | '\x0c' => Key.ctrl 'l'
        | '\x0e' => Key.ctrl 'n'
        | '\x0f' => Key.ctrl 'o'
        | '\x10' => Key.ctrl 'p'
        | '\x11' => Key.ctrl 'q'
        | '\x12' => Key.ctrl 'r'
        | '\x13' => Key.ctrl 's'
        | '\x14' => Key.ctrl 't'
        | '\x15' => Key.ctrl 'u'
        | '\x16' => Key.ctrl 'v'
        | '\x17' => Key.ctrl 'w'
        | '\x18' => Key.ctrl 'x'
        | '\x19' => Key.ctrl 'y'
        | '\x1a' => Key.ctrl 'z'
        | '\x7f' => Key.backspace
        | '\x0a' | '\x0d' => Key.enter
        | _ => Key.char c
       (state, [k])
/-- Check for escape sequence timeout. -/
def checkTimeout (state : EditorState) (currentTime : Nat) : (EditorState × List Key) :=
  if state.inputState.pendingKeys.length > 0 then
    if currentTime - state.inputState.lastInputTime > 50 then -- 50ms timeout
       -- Timeout! Flush pending keys as is.
       let keys := state.inputState.pendingKeys.toList.map (fun x => if x == '\x1b' then Key.esc else Key.char x)
       ({ state with inputState := { state.inputState with pendingKeys := "" } }, keys)
    else
       (state, [])
  else
    (state, [])
def enforceScroll (state : EditorState) : EditorState :=
  let (h, w) := state.getActiveWindowBounds
  -- Active window height. Reserve 1 line for status bar?
  -- UI logic reserves 1 for status bar in split rendering.
  let linesInView := if h > 1 then h - 1 else 1
  -- Vertical Scroll
  let (sRow, sCol) := state.getScroll
  let cursor := state.getCursor
  let state :=
    if cursor.row.val < sRow.val then
      state.setScroll cursor.row sCol
    else if cursor.row.val >= sRow.val + linesInView then
      let newScrollRow : Row := ⟨cursor.row.val - linesInView + 1⟩
      state.setScroll newScrollRow sCol
    else
      state
  -- Refresh scroll after potential update
  let (sRow, sCol) := state.getScroll
  -- Horizontal Scroll
  let lnWidth := if state.config.showLineNumbers then 4 else 0
  let colsInView := if w > lnWidth then w - lnWidth else 1
  let state :=
    if cursor.col.val < sCol.val then
      state.setScroll sRow cursor.col
    else if cursor.col.val >= sCol.val + colsInView then
      let newScrollCol : Col := ⟨cursor.col.val - colsInView + 1⟩
      state.setScroll sRow newScrollCol
    else
      state
  state
def update (config : Config) (state : EditorState) (k : Key) : IO EditorState := do
  let newState ← match state.mode with
  | .normal => config.bindings.normal state k
  | .insert => config.bindings.insert state k
  | .command => config.bindings.command state k
  | .visual => config.bindings.visual state k
  | .visualBlock => config.bindings.visualBlock state k
  return enforceScroll newState
end ViE

import ViE.Command.Dispatch
import ViE.Command.Impl
import ViE.Command.Parser

namespace ViE.Command
/-- Parse filename argument from command args.
    Returns the filename from args, or the current buffer's filename if no args provided.
    Returns error message if multiple args or no filename available. -/
def parseFilenameArg (args : List String) (currentFilename : Option String) : Except String String :=
  match args with
  | [fname] => .ok fname
  | [] => match currentFilename with
    | some fname => .ok fname
    | none => .error "No file name"
  | _ => .error "Too many arguments"
end ViE.Command

import ViE.State
import ViE.Types
import ViE.Window.Actions
import ViE.Buffer.Manager
import ViE.Command.Explorer
import ViE.Loader
import ViE.Checkpoint
import ViE.Command.Parser
namespace ViE.Command
open ViE.Window
open ViE.Buffer
open ViE.Feature
def cmdEdit (args : List String) (state : EditorState) : IO EditorState := do
  match args with
  | [fname] =>
    -- Resolve path relative to workspace
    let resolvedPath := state.workspace.resolvePath fname
    ViE.Buffer.openBuffer state resolvedPath
  | [] => return { state with message := "No file name" }
  | _ => return { state with message := "Too many arguments" }
def cmdWrite (args : List String) (state : EditorState) : IO EditorState :=
  match ViE.Command.parseFilenameArg args state.getActiveBuffer.filename with
  | .ok fname =>
    ViE.saveBuffer state fname
  | .error msg =>
    return { state with message := msg }
def cmdQuit (_ : List String) (state : EditorState) : IO EditorState :=
  return (ViE.Window.closeActiveWindow state)
def cmdQuitForce (_ : List String) (state : EditorState) : IO EditorState :=
  return { state with shouldQuit := true }
def cmdWriteQuit (args : List String) (state : EditorState) : IO EditorState := do
  match ViE.Command.parseFilenameArg args state.getActiveBuffer.filename with
  | .ok fname =>
    let state' ← ViE.saveBuffer state fname
    return (ViE.Window.closeActiveWindow state')
  | .error msg =>
    return { state with message := msg }
def cmdSplit (_ : List String) (state : EditorState) : IO EditorState :=
  return ViE.Window.splitWindow state true
def cmdVSplit (_ : List String) (state : EditorState) : IO EditorState :=
  return ViE.Window.splitWindow state false
def cmdSet (args : List String) (state : EditorState) : IO EditorState :=
  match args with
  | ["number"] => return { state with config := { state.config with showLineNumbers := true }, message := "number set" }
  | ["nonumber"] => return { state with config := { state.config with showLineNumbers := false }, message := "number unset" }
  | _ => return { state with message := s!"Unknown setting or args: {args}" }
def cmdWincmd (args : List String) (state : EditorState) : IO EditorState :=
  match args with
  | ["w"] => return ViE.Window.cycleWindow state
  | ["h"] => return ViE.Window.switchWindow state .left
  | ["j"] => return ViE.Window.switchWindow state .down
  | ["k"] => return ViE.Window.switchWindow state .up
  | ["l"] => return ViE.Window.switchWindow state .right
  | ["s"] => return ViE.Window.splitWindow state true
  | ["v"] => return ViE.Window.splitWindow state false
  | ["q"] => return (ViE.Window.closeActiveWindow state)
  | _ => return { state with message := s!"Unknown wincmd: {args}" }
def cmdWinLeft (_ : List String) (state : EditorState) : IO EditorState := return ViE.Window.switchWindow state .left
def cmdWinDown (_ : List String) (state : EditorState) : IO EditorState := return ViE.Window.switchWindow state .down
def cmdWinUp (_ : List String) (state : EditorState) : IO EditorState := return ViE.Window.switchWindow state .up
def cmdWinRight (_ : List String) (state : EditorState) : IO EditorState := return ViE.Window.switchWindow state .right
def cmdWinCycle (_ : List String) (state : EditorState) : IO EditorState := return ViE.Window.cycleWindow state
def cmdCd (args : List String) (state : EditorState) : IO EditorState :=
  match args with
  | [path] =>
    -- Change workspace
    let absPath := if path.startsWith "/" then path
                   else match state.workspace.rootPath with
                        | some root => root ++ "/" ++ path
                        | none => path
    return { state with
      workspace := { rootPath := some absPath },
      message := s!"Workspace: {absPath}"
    }
  | [] =>
    -- Clear workspace
    return { state with
      workspace := defaultWorkspace,
      message := "Workspace cleared"
    }
  | _ => return { state with message := "Usage: :cd [path]" }
def cmdPwd (_ : List String) (state : EditorState) : IO EditorState :=
  match state.workspace.rootPath with
  | some path => return { state with message := path }
  | none => return { state with message := "No workspace set" }
def cmdWg (args : List String) (state : EditorState) : IO EditorState :=
  match args with
  | [n] =>
    match n.toNat? with
    | some num =>
      if num < 10 then
        let s' := state.switchToWorkgroup num
        return { s' with message := s!"Switched to workgroup {num}" }
      else
        return { state with message := "Workgroup number must be 0-9" }
    | none => return { state with message := "Invalid workgroup number" }
  | [] => return { state with message := s!"Current workgroup: {state.currentGroup}" }
  | _ => return { state with message := "Usage: :wg [0-9]" }
def cmdExplorer (args : List String) (state : EditorState) : IO EditorState :=
  let path := match args with
     | [] => state.workspace.rootPath.getD "."
     | [p] => p
     | _ => "."
  ViE.Feature.openExplorer state path
def cmdReload (_ : List String) (state : EditorState) : IO EditorState := do
  let success ← ViE.Loader.buildConfig
  if success then
    -- Save session
    ViE.Checkpoint.saveSession state
    -- Restart
    ViE.Loader.restartEditor []
    return { state with shouldQuit := true }
  else
    return { state with message := "Configuration build failed" }
def defaultCommandMap : CommandMap := [
  ("e", cmdEdit),
  ("w", cmdWrite),
  ("q", cmdQuit),
  ("q!", cmdQuitForce),
  ("qa", cmdQuitForce),
  ("qa!", cmdQuitForce),
  ("wq", cmdWriteQuit),
  ("sp", cmdSplit),
  ("split", cmdSplit),
  ("hs", cmdSplit),
  ("hsplit", cmdSplit),
  ("vs", cmdVSplit),
  ("vsplit", cmdVSplit),
  ("set", cmdSet),
  ("wincmd", cmdWincmd),
  ("wh", cmdWinLeft),
  ("wj", cmdWinDown),
  ("wk", cmdWinUp),
  ("wl", cmdWinRight),
  ("wc", cmdWinCycle),
  ("cd", cmdCd),
  ("pwd", cmdPwd),
  ("wg", cmdWg),
  ("ee", cmdExplorer),
  ("reload", cmdReload),
  ("refresh", cmdReload)
]
end ViE.Command

import ViE.State
import ViE.Types
import ViE.Buffer.Manager
import ViE.Basic
namespace ViE.Feature
open ViE
/-- Open the file explorer at the specified path (or current workspace root) -/
def openExplorer (state : EditorState) (pathArg : String) : IO EditorState := do
  let path := if pathArg == "." || pathArg == "" then state.workspace.rootPath.getD "."
              else if pathArg.startsWith "/" then pathArg
              else match state.workspace.rootPath with
                   | some root => root ++ "/" ++ pathArg
                   | none => pathArg
  -- Read directory contents
  try
    let dirPath := System.FilePath.mk path
    let entries := (← System.FilePath.readDir dirPath).toList
    let mut fileEntries : List FileEntry := []
    -- Add parent directory entry if not at root
    if path != "/" then
      let parentPath := match dirPath.parent with
        | some p => p.toString
        | none => "/"
      fileEntries := fileEntries ++ [{
        name := ".."
        path := parentPath
        isDirectory := true
      }]
    -- Convert directory entries to FileEntry
    for entry in entries do
      let entryPath := entry.path.toString
      let isDir ← entry.path.isDir
      fileEntries := fileEntries ++ [{
        name := entry.fileName
        path := entryPath
        isDirectory := isDir
      }]
    -- Sort: directories first, then files, alphabetically
    let sortedEntries := fileEntries.toArray.qsort fun a b =>
      if a.isDirectory != b.isDirectory then
        a.isDirectory -- directories first
      else
        a.name < b.name
    -- Create explorer state
    let explorerState : ExplorerState := {
      currentPath := path
      entries := sortedEntries.toList
      selectedIndex := 0
    }
    -- Generate buffer content
    let header := [s!"Explorer: {path}", ""]
    let mut content := header
    let mut idx := 0
    for entry in explorerState.entries do
      let pref := if idx == 0 then "> " else "  "
      let icon := if entry.isDirectory then state.config.dirIcon else state.config.fileIcon
      let suffix := if entry.isDirectory then "/" else ""
      content := content ++ [s!"{pref}{icon}{entry.name}{suffix}"]
      idx := idx + 1
     -- Create new buffer
    let contentBuffer := content.toArray.map stringToLine
    let (bufferId, s') := ViE.Buffer.createNewBuffer state contentBuffer (some s!"explorer://{path}")
    -- Register explorer
    let s'' := { s' with explorers := (bufferId, explorerState) :: s'.explorers }
    -- Switch to explorer buffer
    let s''' := s''.updateActiveView fun v => { v with bufferId := bufferId, cursor := {row := 2, col := 0}, scrollRow := 0, scrollCol := 0 }
    return { s''' with message := s!"Explorer: {path}" }
  catch e =>
    return { state with message := s!"Error reading directory: {e}" }
/-- Handle Enter key in explorer buffer -/
def handleExplorerEnter (state : EditorState) : IO EditorState := do
  let buf := state.getActiveBuffer
  -- Check if this is an explorer buffer
  let explorerOpt := state.explorers.find? (fun (id, _) => id == buf.id)
  match explorerOpt with
  | none => return state.insertNewline -- Not an explorer, normal behavior
  | some (_, explorer) =>
    -- Get current cursor row
    let cursor := state.getCursor
    -- Explorer header is 2 lines, so subtract 2
    let selectedIdx := cursor.row - 2
    if selectedIdx < 0 || selectedIdx >= explorer.entries.length then
      return state
    -- Get selected entry
    let entry := explorer.entries[selectedIdx]!
    if entry.isDirectory then
      -- Navigate to directory
      openExplorer state entry.path
    else
      -- Open file
      ViE.Buffer.openBuffer state entry.path
end ViE.Feature

import ViE.State
import ViE.IO
import ViE.Loader
import ViE.Checkpoint
import ViE.Types
import ViE.Buffer.Content
import ViE.Window.Actions
import ViE.Window.Analysis
import ViE.Buffer.Manager
import ViE.Command.Explorer
import ViE.Command.Parser
open ViE.Window
open ViE.Buffer
open ViE.Feature
open ViE.Command
namespace ViE.Command
def executeCommand (commands : CommandMap) (state : EditorState) : IO EditorState := do
  let fullCmd := state.inputState.commandBuffer
  let parts := fullCmd.splitOn " "
  match parts with
  | [] => return state
  | cmd :: args =>
    match commands.lookup cmd with
    | some action => action args state
    | none => return { state with message := s!"Unknown command: {fullCmd}" }
end ViE.Command

namespace ViE.Color
/-- Represents terminal colors. -/
inductive Color
  | black | red | green | yellow | blue | magenta | cyan | white
  | brightBlack | brightRed | brightGreen | brightYellow | brightBlue | brightMagenta | brightCyan | brightWhite
  | rgb (r g b : UInt8)
  | grayscale (level : UInt8) -- 0-23 (maps to 232-255)
  | default
  deriving Repr, BEq, Inhabited
/-- Convert Color to FG ANSI string -/
def toFg (c : Color) : String :=
  match c with
  | .black => "\x1b[30m"
  | .red => "\x1b[31m"
  | .green => "\x1b[32m"
  | .yellow => "\x1b[33m"
  | .blue => "\x1b[34m"
  | .magenta => "\x1b[35m"
  | .cyan => "\x1b[36m"
  | .white => "\x1b[37m"
  | .brightBlack => "\x1b[90m"
  | .brightRed => "\x1b[91m"
  | .brightGreen => "\x1b[92m"
  | .brightYellow => "\x1b[93m"
  | .brightBlue => "\x1b[94m"
  | .brightMagenta => "\x1b[95m"
  | .brightCyan => "\x1b[96m"
  | .brightWhite => "\x1b[97m"
  | .rgb r g b => s!"\x1b[38;2;{r};{g};{b}m"
  | .grayscale level =>
      let idx := 232 + (if level > 23 then 23 else level)
      s!"\x1b[38;5;{idx}m"
  | .default => "\x1b[39m"
/-- Convert Color to BG ANSI string -/
def toBg (c : Color) : String :=
  match c with
  | .black => "\x1b[40m"
  | .red => "\x1b[41m"
  | .green => "\x1b[42m"
  | .yellow => "\x1b[43m"
  | .blue => "\x1b[44m"
  | .magenta => "\x1b[45m"
  | .cyan => "\x1b[46m"
  | .white => "\x1b[47m"
  | .brightBlack => "\x1b[100m"
  | .brightRed => "\x1b[101m"
  | .brightGreen => "\x1b[102m"
  | .brightYellow => "\x1b[103m"
  | .brightBlue => "\x1b[104m"
  | .brightMagenta => "\x1b[105m"
  | .brightCyan => "\x1b[106m"
  | .brightWhite => "\x1b[107m"
  | .rgb r g b => s!"\x1b[48;2;{r};{g};{b}m"
  | .grayscale level =>
      let idx := 232 + (if level > 23 then 23 else level)
      s!"\x1b[48;5;{idx}m"
  | .default => "\x1b[49m"
def reset : String := "\x1b[0m"
/-- Helper to parse hex string like "#RRGGBB" or "RRGGBB". -/
def fromHex (hex : String) : Option Color :=
  let s := if hex.startsWith "#" then hex.drop 1 else hex
  if s.positions.count != 6 then none
  else
    let rStr := s.take 2
    let gStr := (s.drop 2).take 2
    let bStr := (s.drop 4).take 2
    match (String.toNat? ("0x" ++ rStr)), (String.toNat? ("0x" ++ gStr)), (String.toNat? ("0x" ++ bStr)) with
    | some r, some g, some b =>
       if r < 256 && g < 256 && b < 256 then
         some (.rgb r.toUInt8 g.toUInt8 b.toUInt8)
       else none
    | _, _, _ => none
end ViE.Color

import ViE.State
import ViE.IO
namespace ViE.Checkpoint
def sessionFile : String := "/tmp/editor_session.tmp"
/-- Save current session state to a temporary file. -/
def saveSession (state : EditorState) : IO Unit := do
  let wg := state.getCurrentWorkgroup
  let buffers := wg.buffers.filter (fun b => b.filename.isSome)
  let activeBuffer := state.getActiveBuffer
  let activeIdx := buffers.findIdx? (fun b => b.id == activeBuffer.id) |>.getD 0
  -- Create content:
  -- FILE1
  -- ROW COL
  -- ...
  -- --ACTIVE--
  -- INDEX
  let mut content := ""
  for b in buffers do
    content := content ++ b.filename.get! ++ "\n"
    if b.id == activeBuffer.id then
       let cursor := state.getCursor
       content := content ++ s!"{cursor.row} {cursor.col}\n"
    else
       content := content ++ "0 0\n"
  content := content ++ "--ACTIVE--\n"
  content := content ++ s!"{activeIdx}\n"
  IO.FS.writeFile sessionFile content
/-- Load session state from temporary file. -/
def loadSession : IO (Option (List String × Nat × List (Nat × Nat))) := do
  if ← System.FilePath.pathExists sessionFile then
    let content ← IO.FS.readFile sessionFile
    -- Clean up the file immediately so next run doesn't pick it up if not intended
    IO.FS.removeFile sessionFile
    let lines := content.splitOn "\n"
    let rec parseFiles (lines : List String) (accFiles : List String) (accCursors : List (Nat × Nat)) : Option (List String × Nat × List (Nat × Nat)) :=
      match lines with
      | [] => none
      | "--ACTIVE--" :: idxStr :: _ =>
        let idx := idxStr.toNat!
        some (accFiles.reverse, idx, accCursors.reverse)
      | fname :: coords :: rest =>
        let parts := coords.splitOn " "
        match parts with
        | [r, c] =>
           let cursor := (r.toNat!, c.toNat!)
           parseFiles rest (fname :: accFiles) (cursor :: accCursors)
        | _ => none -- Parse error
      | _ => none
    return parseFiles lines [] []
  else
    return none
end ViE.Checkpoint

import ViE.Buffer.Manager
import ViE.Buffer.Content

import ViE.State
import ViE.Types
import ViE.Buffer.Content
import ViE.Buffer.LowIO
namespace ViE.Buffer
open ViE
def createNewBuffer (state : EditorState) (content : TextBuffer) (filename : Option String) : (Nat × EditorState) :=
  let s' := state.updateCurrentWorkgroup fun wg =>
    let id := wg.nextBufferId
    let buf : FileBuffer := ViE.Buffer.fileBufferFromTextBuffer id filename content
    { wg with buffers := buf :: wg.buffers, nextBufferId := id + 1 }
  let wg := s'.getCurrentWorkgroup
  (wg.nextBufferId - 1, s')
def findBufferByFilename (state : EditorState) (fname : String) : Option Nat :=
  let wg := state.getCurrentWorkgroup
  wg.buffers.find? (fun b => b.filename == some fname) |>.map (fun b => b.id)
/-- Open a file buffer in the active window. Loads from disk if necessary. -/
def openBuffer (state : EditorState) (filename : String) : IO EditorState := do
  let resolvedPath := state.workspace.resolvePath filename
  match findBufferByFilename state resolvedPath with
  | some bid =>
    -- Switch to existing buffer
    let s' := state.updateActiveView fun v => { v with bufferId := bid, cursor := {row:=0, col:=0}, scrollRow:=0, scrollCol:=0 }
    return { s' with message := s!"Switched to \"{filename}\"" }
  | none =>
    try
      let loadedBuf ← ViE.loadBufferByteArray resolvedPath
      -- Assign new ID and add to workgroup
      let s' := state.updateCurrentWorkgroup fun wg =>
        let id := wg.nextBufferId
        let buf := { loadedBuf with id := id }
        { wg with buffers := buf :: wg.buffers, nextBufferId := id + 1 }
      let wg := s'.getCurrentWorkgroup
      let bid := wg.nextBufferId - 1
      let s'' := s'.updateActiveView fun v => { v with bufferId := bid, cursor := {row:=0, col:=0}, scrollRow:=0, scrollCol:=0 }
      return { s'' with message := s!"Loaded \"{filename}\"" }
    catch e =>
      return { state with message := s!"Error loading file: {e}" }
end ViE.Buffer

import ViE.Types
import ViE.Data.PieceTable
namespace ViE
open ViE.PieceTable
/-- Load buffer from file using PieceTable -/
def loadBufferByteArray (filename : String) : IO FileBuffer := do
  try
    let path := System.FilePath.mk filename
    if ← path.pathExists then
      if ← path.isDir then
        -- Directory: return empty buffer
        return {
          id := 0
          filename := some filename
          dirty := false
          table := PieceTable.fromString ""
          missingEol := false
        }
      else
        -- Read file as ByteArray
        let data ← IO.FS.readBinFile filename
        -- Check if file ends with newline (POSIX compliance)
        let missingEol := data.size > 0 && data[data.size - 1]! != 10
        let table := PieceTable.fromByteArray data
        return {
          id := 0
          filename := some filename
          dirty := false
          table := table
          missingEol := missingEol
        }
    else
      -- File doesn't exist, return empty buffer
      return {
        id := 0
        filename := some filename
        dirty := false
        table := PieceTable.fromString ""
        missingEol := false
      }
  catch _ =>
    -- On error, return empty buffer
    return {
      id := 0
      filename := some filename
      dirty := false
      table := PieceTable.fromString ""
      missingEol := false
    }
end ViE

import ViE.Types
import ViE.Basic
import ViE.Data.PieceTable
namespace ViE
open ViE.PieceTable
/-- Get a line from FileBuffer (delegates to PieceTable) -/
def getLineFromBuffer (buffer : FileBuffer) (n : Nat) : Option String :=
  buffer.table.getLine n
/-- Get line length from FileBuffer (delegates to PieceTable) -/
def getLineLengthFromBuffer (buffer : FileBuffer) (n : Nat) : Option Nat :=
  buffer.table.getLineLength n
namespace Buffer
/-- Convert FileBuffer to TextBuffer (compatibility function) -/
def fileBufferToTextBuffer (buf : FileBuffer) : TextBuffer :=
  let lineCount := FileBuffer.lineCount buf
  if lineCount > 0 then
    -- Map each line index to its string content
    (List.range lineCount).toArray.map fun i =>
      match getLineFromBuffer buf i with
      | some str => stringToLine str
      | none => #[]
  else
    -- Empty buffer - return single empty line
    #[#[]]
/-- Create/Update FileBuffer from TextBuffer (flattening is expensive, avoided if possible) -/
def fileBufferFromTextBuffer (id : Nat) (filename : Option String) (content : TextBuffer) : FileBuffer :=
  let fullString := String.intercalate "\n" (content.toList.map lineToString)
  let table := PieceTable.fromString fullString
  {
    id := id
    filename := filename
    dirty := true -- Assume dirty if created from manual content
    table := table
    missingEol := false -- Default
  }
/-- Update FileBuffer from TextBuffer (compatibility function) -/
def fileBufferUpdateFromTextBuffer (buf : FileBuffer) (newContent : TextBuffer) : FileBuffer :=
  let newBuf := fileBufferFromTextBuffer buf.id buf.filename newContent
  { newBuf with dirty := true }
end Buffer
/-- Modify a line in FileBuffer using PieceTable operations -/
def modifyLineInBuffer (buffer : FileBuffer) (row : Nat) (f : String → String) : FileBuffer :=
  match buffer.table.getLineRange row with
  | some (startOffset, length) =>
     match buffer.table.getLine row with
     | some oldLine =>
        let newLine := f oldLine
        -- Edit: Delete old line content, insert new content.
        -- We preserve the newline character if it exists (getLineRange excludes it).
        let table' := buffer.table.delete startOffset length
        let table'' := table'.insert startOffset newLine
        { buffer with
          table := table''
          dirty := true
        }
     | none => buffer -- Should check range first, but safe fallback
  | none => buffer -- Line not found
end ViE

import ViE.Types
namespace ViE
/-- Convert String to Line (Array Char) -/
def stringToLine (s : String) : Line :=
  s.toList.toArray
/-- Convert Line (Array Char) to String -/
def lineToString (line : Line) : String :=
  String.ofList line.toList
/-- Empty buffer with one empty line -/
def emptyTextBuffer : TextBuffer :=
  #[#[]]
/-- Helper to safely get a line as String. -/
def getLine (buffer : TextBuffer) (n : Nat) : Option String :=
  if h : n < buffer.size then
    some (lineToString buffer[n])
  else
    none
/-- Helper to update a specific line in the buffer. -/
def modifyLine (buffer : TextBuffer) (row : Nat) (f : String → String) : TextBuffer :=
  if h : row < buffer.size then
    let oldLine := buffer[row]
    let newLine := stringToLine (f (lineToString oldLine))
    buffer.set! row newLine
  else
    buffer
/-- Set a line directly (String version for compatibility) -/
def setLine (buffer : TextBuffer) (row : Nat) (content : String) : TextBuffer :=
  buffer.set! row (stringToLine content)
/-- Take first n elements from Array -/
def arrayTake {α : Type _} (arr : Array α) (n : Nat) : Array α :=
  arr.extract 0 n
/-- Drop first n elements from Array -/
def arrayDrop {α : Type _} (arr : Array α) (n : Nat) : Array α :=
  arr.extract n arr.size
/-- Concatenate multiple arrays -/
def arrayConcat {α : Type _} (arrays : List (Array α)) : Array α :=
  arrays.foldl (· ++ ·) #[]
end ViE

import ViE.Basic
import ViE.State
import ViE.Terminal
import ViE.UI
import ViE.Actions
import ViE.IO
import ViE.Config
import ViE.Checkpoint
import ViE.Loader
namespace ViE
open ViE.PieceTable
/-- Main event loop. -/
partial def loop (config : Config) (state : EditorState) : IO Unit := do
  -- Only render if state is dirty
  if state.dirty then
    ViE.UI.render state
  -- Reset dirty flag after render (or if it was already clean, keep it clean)
  let state := { state with dirty := false }
  let currentTime ← IO.monoMsNow
  let c ← ViE.Terminal.readKey
  -- Update window size
  let (rows, cols) ← ViE.Terminal.getWindowSize
  let state := { state with windowHeight := rows, windowWidth := cols }
  -- Handle the case where readKey returns None (no input available)
  match c with
  | none =>
    -- Check for timeout
    let (stateAfterTimeout, keys) := ViE.checkTimeout state currentTime
    if keys.isEmpty then
       -- No input and no timeout events, sleep briefly to avoid busy loop
       IO.sleep 10 -- 10ms
       loop config stateAfterTimeout
    else
       -- Process timeout keys (e.g. flushed Esc)
       let mut finalState := stateAfterTimeout
       for key in keys do
         finalState ← ViE.update config finalState key
       if finalState.shouldQuit then
         return ()
       loop config { finalState with dirty := true }
  | some ch =>
    -- Parse the character into keys using the new parseKey function
    let (stateAfterParse, keys) := ViE.parseKey state ch currentTime
    -- Process all returned keys
    let mut finalState := stateAfterParse
    for key in keys do
      finalState ← ViE.update config finalState key
    if finalState.shouldQuit then
      return ()
    loop config { finalState with dirty := true }
/-- Entry point for the editor.
    Accepts a configuration and command line arguments. -/
def start (config : Config) (args : List String) : IO Unit := do
  -- Check for checkpoint session
  let checkpoint ← ViE.Checkpoint.loadSession
  -- Determine initial args (files to open)
  -- If we have a checkpoint and no args, use the checkpoint files.
  -- Otherwise use provided args.
  let (startArgs, _) := match checkpoint with
    | some (files, activeIdx, cursors) =>
       if args.isEmpty then
         (files, some (activeIdx, cursors))
       else
         (args, none)
    | none => (args, none)
  let filename := startArgs.head?
  -- Check if the argument is a directory
  let (workspacePath, actualFilename) ← match filename with
    | some path =>
      let filePath := System.FilePath.mk path
      if ← filePath.pathExists then
        if ← filePath.isDir then
          -- It's a directory, use as workspace
          pure (some path, none)
        else
          -- It's a file
          pure (none, some path)
      else
        -- Path doesn't exist, treat as new file
        pure (none, some path)
    | none => pure (none, none)
  -- Load buffer if file exists
  let initialBuffer ← match actualFilename with
    | some fname => loadBufferByteArray fname
    | none => pure {
        id := 0
        filename := actualFilename
        dirty := false
        table := PieceTable.fromString ""
        missingEol := false
      }
  -- Check if initial load had an error
  let firstLine := getLineFromBuffer initialBuffer 0 |>.getD ""
  let hasError := firstLine.startsWith "Error loading file:"
  let workspace := match workspacePath with
    | some path => { rootPath := some path }
    | none => ViE.defaultWorkspace
  let state := { ViE.initialState with
    config := config.settings,
    workspace := workspace,
    message := if hasError then firstLine
               else match actualFilename with
                 | some f => s!"\"{f}\" [Read]"
                 | none => match workspacePath with
                   | some ws => s!"Workspace: {ws}"
                   | none => "New File"
  }
  -- Update the first workgroup with the initial buffer
  let state := state.updateCurrentWorkgroup fun wg =>
    { wg with buffers := [initialBuffer] }
  ViE.Terminal.enableRawMode
  try
    loop config state
  finally
    ViE.Terminal.disableRawMode
    ViE.Terminal.clearScreen
    IO.println "Bye!"
end ViE

import ViE.State
import ViE.Command
import ViE.Key
import ViE.IO
import ViE.Config
import ViE.Basic
import ViE.Loader
import ViE.Checkpoint
import ViE.Types
import ViE.Window.Actions
import ViE.Buffer.Manager
namespace ViE
/-- Insert a character at the cursor position. -/
def insertAtCursor (state : EditorState) (c : Char) : EditorState :=
  state.insertChar c
/-- Parse filename argument from command args.
    Returns the filename from args, or the current buffer's filename if no args provided.
    Returns error message if multiple args or no filename available. -/
def parseFilenameArg (args : List String) (currentFilename : Option String) : Except String String :=
  match args with
  | [fname] => .ok fname
  | [] => match currentFilename with
    | some fname => .ok fname
    | none => .error "No file name"
  | _ => .error "Too many arguments"
def executeCommand (commands : CommandMap) (state : EditorState) : IO EditorState := do
  let fullCmd := state.inputState.commandBuffer
  let parts := fullCmd.splitOn " "
  match parts with
  | [] => return state
  | cmd :: args =>
    match commands.lookup cmd with
    | some action => action args state
    | none => return { state with message := s!"Unknown command: {fullCmd}" }
/-- Handle Enter key in explorer buffer -/
def handleExplorerEnter (commands : CommandMap) (state : EditorState) : IO EditorState := do
  let buf := state.getActiveBuffer
  -- Check if this is an explorer buffer
  let explorerOpt := state.explorers.find? (fun (id, _) => id == buf.id)
  match explorerOpt with
  | none => return state.insertNewline -- Not an explorer, normal behavior
  | some (_, explorer) =>
    -- Get current cursor row
    let cursor := state.getCursor
    -- Explorer header is 2 lines, so subtract 2
    let selectedIdx := cursor.row - 2
    if selectedIdx < 0 || selectedIdx >= explorer.entries.length then
      return state
    -- Get selected entry
    let entry := explorer.entries[selectedIdx]!
    if entry.isDirectory then
      -- Navigate to directory
      let s' := { state with inputState := { state.inputState with commandBuffer := s!"ee {entry.path}" } }
      executeCommand commands s'
    else
      -- Open file
      let s' := { state with inputState := { state.inputState with commandBuffer := s!"e {entry.path}" } }
      executeCommand commands s'
def handleCommandInput (commands : CommandMap) (state : EditorState) (k : Key) : IO EditorState := do
  match k with
  | Key.esc => return { state with mode := .normal, message := "", inputState := { state.inputState with commandBuffer := "" } }
  | Key.enter =>
    let newState ← executeCommand commands state
    if newState.shouldQuit then
      return newState
    else
      return { newState with mode := .normal, inputState := { newState.inputState with commandBuffer := "" } }
  | Key.backspace =>
    if state.inputState.commandBuffer.length > 0 then
      let newCmd := state.inputState.commandBuffer.dropEnd 1
      return { state with inputState := { state.inputState with commandBuffer := newCmd.toString } }
    else
      return state
  | Key.char c => return { state with inputState := { state.inputState with commandBuffer := state.inputState.commandBuffer.push c } }
  | _ => return state
def clearInput (s : EditorState) : EditorState :=
  { s with inputState := { s.inputState with countBuffer := "", previousKey := none } }
end ViE

# vi'e
### A Vim-like Extensible text editor
(very WIP)
### installation
clone this source and place or symlink this source under the '~/.config/vie/' directory.
`lake build` and `lake exe editor` or add PATH to the '<this source directory>/.lake/build/bin/' directory.
## Features
- Basic text editing
- Line numbers
- Horizontal scrolling
- Vertical scrolling
- Modes
  - Command mode
  - Insert mode
  - Normal mode
  - Visual mode
  - VisualBlock mode
- Split window buffer
- Render UTF-8 characters (partial support)
- Workgroups
- Hot reload(recompile and reload) configuration 
  - place this source and Main.lean in '~/.config/editor/' and :reload
## Keybindings
### Normal Mode
- `h`: Move cursor left
- `j`: Move cursor down
- `k`: Move cursor up
- `l`: Move cursor right
- `i`: Enter Insert Mode
- `:`; Enter Command Mode
- `q`: Enter Command Mode (alias)
- `d`: Delete current line (press twice `dd`)
- `v`: Enter Visual Mode
- `V`: Enter VisualBlock Mode
- `gg`: Move to top of file
- `G`: Move to bottom of file
- `|`: Jump to column (preceded by number)
- `[number]`: Type a number to set count for `|` or `G` command
- `Enter`: Move cursor down
### Insert Mode
- `Esc`: Return to Normal Mode
- `Backspace`: Delete character before cursor
- `Enter`: Insert newline
### Command Mode
- `Esc`: Return to Normal Mode
- `Enter`: Execute command
### Visual/VisualBlock Mode
- `h/j/k/l`: select more
- `Esc`: Return to Normal Mode
## Commands
- `:w`: Save file
- `:q`: Quit window
- `:q!`: force quit
- `:wq`: Save and quit
- `:set number`: Show line numbers
- `:set nonumber`: Hide line numbers
- `:vs`, `:hs`  vertical and horizontal window splitting
- `:wincmd h/j/k/l` change focus select window
- `:wh`, `:wj`, `:wk`, `:wl` change focus select window (alias)
- `:wincmd w`, `:wc` cyclic selection
- `:wg <n>` switch to workgroup <n>
- `:reload`: reload configuration

import ViE
import ViE.Color
open ViE.Color
def customConfig : ViE.EditorConfig := {
  ViE.defaultConfig with
  showLineNumbers := true
  statusBarStyle := (toBg Color.brightBlack) ++ (toFg Color.white)
  fileIcon := "File: "
  dirIcon := "Dir : "
}
def customKeyMap (commands : ViE.CommandMap) : ViE.KeyMap := {
  ViE.Key.makeKeyMap commands with
  normal := fun s k => match k with
    -- Example custom binding: 'X' to quit
    | ViE.Key.char 'X' => pure { s with shouldQuit := true }
    | _ => (ViE.Key.makeKeyMap commands).normal s k
  visual := fun s k => match k with
    | ViE.Key.char 'o' => pure (ViE.Window.cycleWindow s)
    | _ => (ViE.Key.makeKeyMap commands).visual s k
}
def myCustomCommand (_ : List String) (state : ViE.EditorState) : IO ViE.EditorState := do
  return { state with message := "Executed custom command!" }
def main (args : List String) : IO Unit := do
  let myCommands : ViE.CommandMap := [
    ("mycmd", myCustomCommand),
    ("o", ViE.Command.cmdWinCycle)
  ]
  let commands := ViE.Command.defaultCommandMap ++ myCommands
  let config : ViE.Config := {
    settings := customConfig
    bindings := customKeyMap commands
    commands := commands
  }
  ViE.start config args

Copyright 2026 Yuki Otsuka
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS “AS IS” AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

.git
.DS_Store
.lake