leanprover/lean4:v4.28.0

import Lake
open Lake DSL
package bliku
lean_lib Bliku

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

import Bliku.Tui

import Bliku.Tui.Primitives
import Bliku.Tui.Search
import Bliku.Tui.Syntax
import Bliku.Tui.Terminal
import Bliku.Tui.Window
import Bliku.Tui.Model
import Bliku.Tui.Overlay
import Bliku.Tui.Render

import Bliku.Tui.Primitives
namespace Bliku.Tui
structure Cursor where
  row : Nat
  col : Nat
  deriving Repr, BEq, Inhabited
structure ViewState where
  bufferId : Nat
  cursor : Cursor
  scrollRow : Nat
  scrollCol : 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
structure FloatingWindowBorderFlags where
  top : Bool := true
  right : Bool := true
  bottom : Bool := true
  left : Bool := true
  deriving Inhabited
structure WorkspaceView where
  name : String
  layout : Layout
  activeWindowId : Nat
  floatingWindows : List Nat := []
  floatingWindowOffsets : List (Nat × Int × Int) := []
  deriving Inhabited
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)
def Layout.updateView (l : Layout) (id : Nat) (f : ViewState → ViewState) : Layout :=
  let rec go (node : Layout) : Layout × Bool :=
    match node with
    | .window wid v =>
      if wid == id then (.window wid (f v), true) else (node, false)
    | .hsplit left right ratio =>
      let (left', foundLeft) := go left
      if foundLeft then
        (.hsplit left' right ratio, true)
      else
        let (right', foundRight) := go right
        (.hsplit left' right' ratio, foundRight)
    | .vsplit top bottom ratio =>
      let (top', foundTop) := go top
      if foundTop then
        (.vsplit top' bottom ratio, true)
      else
        let (bottom', foundBottom) := go bottom
        (.vsplit top' bottom' ratio, foundBottom)
  (go l).1
def Layout.containsWindow (l : Layout) (windowId : Nat) : Bool :=
  match l with
  | .window wid _ => wid == windowId
  | .hsplit left right _ => left.containsWindow windowId || right.containsWindow windowId
  | .vsplit top bottom _ => top.containsWindow windowId || bottom.containsWindow windowId
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 left' =>
      match right.remove id with
      | none => some left'
      | some right' => some (.hsplit left' right' ratio)
  | .vsplit top bottom ratio =>
    match top.remove id with
    | none => some bottom
    | some top' =>
      match bottom.remove id with
      | none => some top'
      | some bottom' => some (.vsplit top' bottom' ratio)
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
def getAllWindowBounds (l : Layout) (h w : Nat) : List (Nat × Nat × Nat × Nat × Nat) :=
  let rec traverse (node : Layout) (r c h w : Nat) (acc : List (Nat × Nat × Nat × Nat × Nat)) :=
    match node 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 WorkspaceView.isFloatingWindow (ws : WorkspaceView) (windowId : Nat) : Bool :=
  ws.floatingWindows.contains windowId
def WorkspaceView.getFloatingWindowIds (ws : WorkspaceView) : Array Nat :=
  ws.floatingWindows.foldl (fun acc wid =>
    match ws.layout.findView wid with
    | some _ => acc.push wid
    | none => acc) #[]
def WorkspaceView.floatingWindowIndex? (ws : WorkspaceView) (windowId : Nat) : Option Nat :=
  let ids := ws.getFloatingWindowIds
  let rec loop (i : Nat) : Option Nat :=
    if i >= ids.size then none
    else if ids[i]! == windowId then some i
    else loop (i + 1)
  loop 0
def WorkspaceView.getFloatingWindowOffset (ws : WorkspaceView) (windowId : Nat) : Int × Int :=
  match ws.floatingWindowOffsets.find? (fun (wid, _, _) => wid == windowId) with
  | some (_, ro, co) => (ro, co)
  | none => (0, 0)
def computeFloatingWindowBounds (rows cols idx : Nat) : Option (Nat × Nat × Nat × Nat) :=
  let availableRows := if rows > 1 then rows - 1 else rows
  if availableRows < 6 || cols < 16 then
    none
  else
    let hMax := availableRows - 2
    let wMax := cols - 4
    let h := min hMax (max 8 ((availableRows * 3) / 5))
    let w := min wMax (max 24 ((cols * 3) / 5))
    let topBase := (availableRows - h) / 2
    let leftBase := (cols - w) / 2
    let top := min (availableRows - h) (topBase + idx)
    let left := min (cols - w) (leftBase + (2 * idx))
    some (top, left, h, w)
def getFloatingWindowBounds (ws : WorkspaceView) (windowHeight windowWidth : Nat) (windowId : Nat) : Option (Nat × Nat × Nat × Nat) :=
  match ws.floatingWindowIndex? windowId with
  | none => none
  | some idx =>
    match computeFloatingWindowBounds windowHeight windowWidth idx with
    | none => none
    | some (top, left, h, w) =>
      let (rowOff, colOff) := ws.getFloatingWindowOffset windowId
      let toNatNonNeg (v : Int) := if v < 0 then 0 else Int.toNat v
      let availableRows := if windowHeight > 1 then windowHeight - 1 else windowHeight
      let maxTop := if availableRows > h then availableRows - h else 0
      let maxLeft := if windowWidth > w then windowWidth - w else 0
      let rawTop := Int.ofNat top + rowOff
      let rawLeft := Int.ofNat left + colOff
      let top' := min maxTop (toNatNonNeg rawTop)
      let left' := min maxLeft (toNatNonNeg rawLeft)
      some (top', left', h, w)
def getFloatingWindowBorderFlags (_ws : WorkspaceView) (_windowId : Nat) : FloatingWindowBorderFlags :=
  { top := true, right := true, bottom := true, left := true }
end Bliku.Tui

namespace Bliku.Tui.Terminal
/-- Get terminal size (rows, cols). -/
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] => pure (rows.toNat!, cols.toNat!)
  | _ => pure (24, 80)
def moveCursorStr (row col : Nat) : String :=
  s!"\x1b[{row + 1};{col + 1}H"
def hideCursorStr : String := "\x1b[?25l"
def showCursorStr : String := "\x1b[?25h"
def clearLineStr : String := "\x1b[K"
def homeCursorStr : String := "\x1b[H"
def clearScreenStr : String := "\x1b[2J"
end Bliku.Tui.Terminal

import Bliku.Tui.Syntax.Types
import Bliku.Tui.Syntax.Lean
import Bliku.Tui.Syntax.Markdown
namespace Bliku.Tui.Syntax
def highlightLine (filename : Option String) (line : String) : Array Span :=
  match detectLanguage filename with
  | .plain => #[]
  | .lean => highlightLeanLine line
  | .markdown => highlightMarkdownLine line
end Bliku.Tui.Syntax

import Bliku.Tui.Search
namespace Bliku.Tui.Syntax
inductive Language where
  | plain
  | lean
  | markdown
  deriving Repr, BEq, Inhabited
structure Span where
  startByte : Nat
  endByte : Nat
  style : String
  deriving Repr, BEq, Inhabited
-- ANSI bright colors.
def leanKeywordStyle : String := "\x1b[94m"
def leanCommentStyle : String := "\x1b[90m"
def leanStringStyle : String := "\x1b[92m"
def leanNumberStyle : String := "\x1b[95m"
def markdownHeadingStyle : String := "\x1b[96m"
def markdownCodeStyle : String := "\x1b[93m"
def markdownLinkStyle : String := "\x1b[94m"
def markdownEmphasisStyle : String := "\x1b[95m"
def detectLanguage (filename : Option String) : Language :=
  match filename with
  | none => .plain
  | some name =>
      if name.endsWith ".lean" then .lean
      else if name.endsWith ".md" || name.endsWith ".markdown" then .markdown
      else .plain
def styleForByteRange (spans : Array Span) (byteStart byteEnd : Nat) : Option String :=
  let rec loop (i : Nat) : Option String :=
    if i >= spans.size then
      none
    else
      let s := spans[i]!
      if Bliku.Tui.overlapsByteRange (s.startByte, s.endByte) byteStart byteEnd then
        some s.style
      else
        loop (i + 1)
  loop 0
end Bliku.Tui.Syntax

import Bliku.Tui.Syntax.Types
namespace Bliku.Tui.Syntax
private def isMarkdownHeading (bytes : ByteArray) : Bool := Id.run do
  let n := bytes.size
  let mut i := 0
  while i < n && bytes[i]! == 32 do
    i := i + 1
  if i >= n || bytes[i]! != 35 then
    return false
  let mut j := i
  while j < n && bytes[j]! == 35 do
    j := j + 1
  return j < n && bytes[j]! == 32
private def isMarkdownFence (bytes : ByteArray) : Bool :=
  (bytes.size >= 3 && bytes[0]! == 96 && bytes[1]! == 96 && bytes[2]! == 96) ||
  (bytes.size >= 3 && bytes[0]! == 126 && bytes[1]! == 126 && bytes[2]! == 126)
def highlightMarkdownLine (line : String) : Array Span := Id.run do
  let bytes := line.toUTF8
  let n := bytes.size
  if isMarkdownHeading bytes then
    return #[{ startByte := 0, endByte := n, style := markdownHeadingStyle }]
  if isMarkdownFence bytes then
    return #[{ startByte := 0, endByte := n, style := markdownCodeStyle }]
  let mut spans : Array Span := #[]
  let mut i := 0
  while i < n do
    if bytes[i]! == 96 then
      let mut j := i + 1
      while j < n && bytes[j]! != 96 do
        j := j + 1
      if j < n then
        spans := spans.push { startByte := i, endByte := j + 1, style := markdownCodeStyle }
        i := j + 1
      else
        i := i + 1
    else if bytes[i]! == 91 then
      let mut j := i + 1
      while j < n && bytes[j]! != 93 do
        j := j + 1
      if j + 1 < n && bytes[j]! == 93 && bytes[j + 1]! == 40 then
        let mut k := j + 2
        while k < n && bytes[k]! != 41 do
          k := k + 1
        if k < n then
          spans := spans.push { startByte := i, endByte := k + 1, style := markdownLinkStyle }
          i := k + 1
        else
          i := i + 1
      else
        i := i + 1
    else if bytes[i]! == 42 || bytes[i]! == 95 then
      let delim := bytes[i]!
      let mut j := i + 1
      while j < n && bytes[j]! != delim do
        j := j + 1
      if j < n && j > i + 1 then
        spans := spans.push { startByte := i, endByte := j + 1, style := markdownEmphasisStyle }
        i := j + 1
      else
        i := i + 1
    else
      i := i + 1
  return spans
end Bliku.Tui.Syntax

import Bliku.Tui.Syntax.Types
namespace Bliku.Tui.Syntax
private def isAsciiLower (n : Nat) : Bool := 97 <= n && n <= 122
private def isAsciiUpper (n : Nat) : Bool := 65 <= n && n <= 90
private def isAsciiDigit (n : Nat) : Bool := 48 <= n && n <= 57
private def isIdentStart (b : UInt8) : Bool :=
  let n := b.toNat
  isAsciiLower n || isAsciiUpper n || n == 95
private def isIdentCont (b : UInt8) : Bool :=
  let n := b.toNat
  isIdentStart b || isAsciiDigit n || n == 39
private def leanKeywords : Array String := #[
  "abbrev", "axiom", "by", "class", "constant", "def", "deriving", "do",
  "else", "end", "example", "from", "have", "if", "import", "in", "inductive",
  "instance", "let", "match", "mutual", "namespace", "open", "opaque", "private",
  "protected", "set_option", "show", "structure", "syntax", "termination_by",
  "theorem", "unsafe", "variable", "where", "with"
]
def highlightLeanLine (line : String) : Array Span := Id.run do
  let bytes := line.toUTF8
  let n := bytes.size
  let mut spans : Array Span := #[]
  let mut i := 0
  while i < n do
    let b := bytes[i]!
    if b == 34 then
      let mut j := i + 1
      let mut escaped := false
      let mut closed := false
      while j < n && !closed do
        let c := bytes[j]!
        if escaped then
          escaped := false
          j := j + 1
        else if c == 92 then
          escaped := true
          j := j + 1
        else if c == 34 then
          closed := true
          j := j + 1
        else
          j := j + 1
      spans := spans.push { startByte := i, endByte := j, style := leanStringStyle }
      i := j
    else if i + 1 < n && bytes[i]! == 45 && bytes[i + 1]! == 45 then
      spans := spans.push { startByte := i, endByte := n, style := leanCommentStyle }
      i := n
    else if i + 1 < n && bytes[i]! == 47 && bytes[i + 1]! == 45 then
      spans := spans.push { startByte := i, endByte := n, style := leanCommentStyle }
      i := n
    else if isAsciiDigit b.toNat then
      let mut j := i + 1
      while j < n do
        let c := bytes[j]!.toNat
        if isAsciiDigit c || c == 95 || c == 46 || c == 120 || c == 111 || c == 98 ||
           (65 <= c && c <= 70) || (97 <= c && c <= 102) then
          j := j + 1
        else
          break
      spans := spans.push { startByte := i, endByte := j, style := leanNumberStyle }
      i := j
    else if isIdentStart b then
      let mut j := i + 1
      while j < n && isIdentCont (bytes[j]!) do
        j := j + 1
      let tok := String.fromUTF8! (bytes.extract i j)
      if leanKeywords.contains tok then
        spans := spans.push { startByte := i, endByte := j, style := leanKeywordStyle }
      i := j
    else
      i := i + 1
  return spans
end Bliku.Tui.Syntax

namespace Bliku.Tui
/-- Find all occurrences of a byte pattern within a byte array. -/
def findAllMatchesBytes (haystack : ByteArray) (needle : ByteArray) : Array (Nat × Nat) := Id.run do
  let n := needle.size
  let h := haystack.size
  if n == 0 || h < n then
    return #[]
  let limit := h - n + 1
  let mut out : Array (Nat × Nat) := #[]
  for i in [0:limit] do
    let mut matched := true
    for j in [0:n] do
      if matched && haystack[i + j]! != needle[j]! then
        matched := false
    if matched then
      out := out.push (i, i + n)
  return out
def overlapsByteRange (r : Nat × Nat) (byteStart byteEnd : Nat) : Bool :=
  let (s, e) := r
  byteStart < e && byteEnd > s
def activeMatchRange (hitRanges : Array (Nat × Nat)) (cursorByte : Option Nat) : Option (Nat × Nat) :=
  match cursorByte with
  | none => none
  | some cb =>
      let rec loop (i : Nat) : Option (Nat × Nat) :=
        if i >= hitRanges.size then
          none
        else
          let m := hitRanges[i]!
          let (s, e) := m
          if s <= cb && cb < e then
            some m
          else
            loop (i + 1)
      loop 0
end Bliku.Tui

import Bliku.Tui.Primitives
import Bliku.Tui.Model
import Bliku.Tui.Window
import Bliku.Tui.Overlay
import Bliku.Tui.Terminal
namespace Bliku.Tui
open Bliku.Tui.Terminal
private def renderLineSlice (line : String) (scrollCol width : Nat) : String :=
  ((line.drop scrollCol).take width).toString
private def getBufferLine (buf : BufferState) (row : Nat) : String :=
  buf.lines[row]?.getD ""
private def isVisualMode (mode : Mode) : Bool :=
  mode == .visual || mode == .visualBlock
private def normalizeCursorRange (a b : Cursor) : Cursor × Cursor :=
  if a.row < b.row || (a.row == b.row && a.col <= b.col) then (a, b) else (b, a)
private def isInSelection (m : Model) (cur : Cursor) (row col : Nat) : Bool :=
  if !isVisualMode m.mode then
    false
  else
    match m.selectionStart with
    | none => false
    | some start =>
      if m.mode == .visualBlock then
        let minRow := min start.row cur.row
        let maxRow := max start.row cur.row
        let minCol := min start.col cur.col
        let maxCol := max start.col cur.col
        row >= minRow && row <= maxRow && col >= minCol && col <= maxCol
      else
        let (p1, p2) := normalizeCursorRange start cur
        if row < p1.row || row > p2.row then false
        else if row > p1.row && row < p2.row then true
        else if p1.row == p2.row then col >= p1.col && col <= p2.col
        else if row == p1.row then col >= p1.col
        else if row == p2.row then col <= p2.col
        else false
private def styleVisibleLine
    (m : Model) (windowId lineIdx scrollCol : Nat) (visible : String) (windowCursor : Option Cursor) : String := Id.run do
  let activeRow := windowCursor.map (fun c => c.row) |>.getD 0
  let activeCol := windowCursor.map (fun c => c.col) |>.getD 0
  let selectionCur := windowCursor.getD { row := lineIdx, col := scrollCol }
  let mut out : Array String := #[]
  let mut activeStyle : Option String := none
  let chars := visible.toList
  let mut i := 0
  for ch in chars do
    let col := scrollCol + i
    let isCursor :=
      windowId == m.workspace.activeWindowId &&
      lineIdx == activeRow &&
      col == activeCol
    let desiredStyle : Option String :=
      if isCursor then
        if ch == ' ' then some m.config.cursorSpaceStyle else some m.config.cursorCharStyle
      else if isInSelection m selectionCur lineIdx col then
        some m.config.visualSelectionStyle
      else
        none
    if desiredStyle != activeStyle then
      match activeStyle with
      | some _ => out := out.push m.config.resetStyle
      | none => pure ()
      match desiredStyle with
      | some stl => out := out.push stl
      | none => pure ()
      activeStyle := desiredStyle
    out := out.push ch.toString
    i := i + 1
  if activeStyle.isSome then
    out := out.push m.config.resetStyle
  return String.intercalate "" out.toList
private def appendCursorOnBlankCell
    (m : Model) (windowId lineIdx scrollCol availableWidth : Nat)
    (visible : String) (lineToDraw : String) (windowCursor : Option Cursor) : String := Id.run do
  let some cur := windowCursor | return lineToDraw
  if windowId != m.workspace.activeWindowId || lineIdx != cur.row || cur.col < scrollCol then
    return lineToDraw
  let visCol := cur.col - scrollCol
  let visLen := visible.toList.length
  if visCol < visLen || visCol >= availableWidth then
    return lineToDraw
  let padCount := visCol - visLen
  return lineToDraw ++ ("".pushn ' ' padCount) ++ m.config.cursorSpaceStyle ++ " " ++ m.config.resetStyle
private def renderWindow (m : Model) (windowId : Nat) (view : ViewState) (rect : Rect) : (Array String × Option (Nat × Nat)) := Id.run do
  let r := rect.row
  let c := rect.col
  let h := rect.height
  let w := rect.width
  let workH := if h > 0 then h - 1 else 0
  let buf := getBuffer m view.bufferId
  let mut out : Array String := #[]
  for i in [0:workH] do
    let lineIdx := view.scrollRow + i
    out := out.push (moveCursorStr (r + i) c)
    if lineIdx < buf.lines.size then
      let lnWidth := if m.config.showLineNumbers then 4 else 0
      let availableWidth := if w > lnWidth then w - lnWidth else 0
      let windowCursor := if windowId == m.workspace.activeWindowId then some view.cursor else none
      if m.config.showLineNumbers then
        out := out.push s!"{leftPad (toString (lineIdx + 1)) 3} "
      let visible := renderLineSlice (getBufferLine buf lineIdx) view.scrollCol availableWidth
      let styled := styleVisibleLine m windowId lineIdx view.scrollCol visible windowCursor
      let lineToDraw := appendCursorOnBlankCell m windowId lineIdx view.scrollCol availableWidth visible styled windowCursor
      out := out.push lineToDraw
    else
      out := out.push m.config.emptyLineMarker
    out := out.push clearLineStr
  let statusRow := r + workH
  out := out.push (moveCursorStr statusRow c)
  let fileName := buf.filename.getD "[No Name]"
  let modeStr := if windowId == m.workspace.activeWindowId then s!"-- {m.mode} --" else "--"
  let eolMark := if buf.missingEol then " [noeol]" else ""
  let statusStr := s!"{modeStr} {fileName}{eolMark} [W:{windowId} B:{view.bufferId}] [{m.workgroupName}] {m.workspace.name}"
  out := out.push m.config.statusBarStyle
  out := out.push statusStr
  out := out.push clearLineStr
  out := out.push m.config.resetStyle
  let cursorPos : Option (Nat × Nat) :=
    if view.cursor.row < view.scrollRow then none
    else
      let visRow := view.cursor.row - view.scrollRow
      if visRow < workH then
        let colOffset := if m.config.showLineNumbers then 4 else 0
        let visCol := if view.cursor.col >= view.scrollCol then view.cursor.col - view.scrollCol else 0
        if visCol + colOffset < w then
          some (r + visRow, c + visCol + colOffset)
        else none
      else none
  (out, cursorPos)
private def renderLayout (m : Model) (l : Layout) (r c h w : Nat) : (Array String × Option (Nat × Nat)) := Id.run do
  match l with
  | .window id view =>
    if m.workspace.isFloatingWindow id then
      let mut blank : Array String := #[]
      for i in [0:h] do
        blank := blank.push (moveCursorStr (r + i) c)
        blank := blank.push ("".pushn ' ' w)
      return (blank, none)
    let (buf, cur) := renderWindow m id view { row := r, col := c, height := h, width := w }
    return (buf, if id == m.workspace.activeWindowId then cur else none)
  | .hsplit left right ratio =>
    let leftW := (Float.ofNat w * ratio).toUInt64.toNat
    let (leftBuf, leftCur) := renderLayout m left r c h leftW
    let mut sep : Array String := #[]
    if w > leftW then
      let sepCol := c + leftW
      for i in [0:h] do
        sep := sep.push (moveCursorStr (r + i) sepCol)
        sep := sep.push m.config.vSplitStr
    let (rightBuf, rightCur) := renderLayout m right r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0)
    return (leftBuf ++ sep ++ rightBuf, rightCur.orElse (fun _ => leftCur))
  | .vsplit top bottom ratio =>
    let topH := (Float.ofNat h * ratio).toUInt64.toNat
    let (topBuf, topCur) := renderLayout m top r c topH w
    let mut sep : Array String := #[]
    if h > topH then
      let sepRow := r + topH
      sep := sep.push (moveCursorStr sepRow c)
      for _ in [0:w] do
        sep := sep.push m.config.hSplitStr
    let (bottomBuf, bottomCur) := renderLayout m bottom (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w
    return (topBuf ++ sep ++ bottomBuf, bottomCur.orElse (fun _ => topCur))
private def renderFloatingWindows (m : Model) : (Array String × Option (Nat × Nat)) := Id.run do
  let ws := m.workspace
  let mut out : Array String := #[]
  let mut activeCur : Option (Nat × Nat) := none
  let ids := ws.getFloatingWindowIds
  for i in [0:ids.size] do
    let wid := ids[i]!
    match ws.layout.findView wid, getFloatingWindowBounds ws m.windowHeight m.windowWidth wid with
    | some view, some (top, left, h, w) =>
      let (buf, cur) := renderWindow m wid view { row := top, col := left, height := h, width := w }
      out := out ++ buf
      if wid == ws.activeWindowId then
        activeCur := cur
    | _, _ => pure ()
  (out, activeCur)
private def findOverlayCursorPos (rows cols : Nat) (m : Model) : Option (Nat × Nat) :=
  match m.floatingOverlay with
  | none => none
  | some ov =>
    match computeFloatingOverlayLayout rows cols ov with
    | none => none
    | some layout =>
      let lines := if ov.lines.isEmpty then #[""] else ov.lines
      let maxRow := lines.size - 1
      let rowIdx := min ov.cursorRow maxRow
      let lineLen := (lines[rowIdx]!).length
      let colIdx := min ov.cursorCol lineLen
      let visRow := min rowIdx (layout.contentRows - 1)
      let visCol := min colIdx layout.innerWidth
      some (layout.top + 1 + layout.titleRows + visRow, layout.left + 2 + visCol)
/-- Render model to terminal and return updated model (size synchronized). -/
def render (model : Model) : IO Model := do
  if !model.dirty then
    return model
  let (rows, cols) ← getWindowSize
  let m := { model with windowHeight := rows, windowWidth := cols }
  let mut buffer : Array String := #[]
  buffer := buffer.push hideCursorStr
  let layoutH := if rows > 0 then rows - 1 else 0
  let baseLayout :=
    m.workspace.getFloatingWindowIds.foldl (fun acc wid =>
      match acc with
      | some l => l.remove wid
      | none => none) (some m.workspace.layout)
  if baseLayout.isNone then
    buffer := buffer.push clearScreenStr
  buffer := buffer.push homeCursorStr
  let (layoutBuf, activeCur) :=
    match baseLayout with
    | some l => renderLayout m l 0 0 layoutH cols
    | none => (#[], none)
  buffer := buffer ++ layoutBuf
  let (floatBuf, floatCur) := renderFloatingWindows m
  buffer := buffer ++ floatBuf
  buffer := buffer.push (moveCursorStr (rows - 1) 0)
  buffer := buffer.push (renderStatusBar m)
  buffer := buffer.push clearLineStr
  let overlayToRender := m.floatingOverlay.orElse (fun _ => messageOverlayForState m)
  if let some ov := overlayToRender then
    buffer := buffer ++ renderFloatingOverlay rows cols ov
  buffer := buffer ++ renderCompletionPopup rows cols m activeCur
  let overlayCur := findOverlayCursorPos rows cols m
  buffer := buffer.push (
    if m.floatingOverlay.isSome && m.mode != .command && m.mode != .searchForward && m.mode != .searchBackward then
      match overlayCur with
      | some (pr, pc) => moveCursorStr pr pc
      | none => ""
    else
      match floatCur.orElse (fun _ => activeCur) with
      | some (pr, pc) => moveCursorStr pr pc
      | none => ""
  )
  if m.mode == .command || m.mode == .searchForward || m.mode == .searchBackward then
    buffer := buffer.push (moveCursorStr (rows - 1) (1 + m.commandBuffer.length))
  if m.mode == .visual || m.mode == .visualBlock then
    buffer := buffer.push hideCursorStr
  else
    buffer := buffer.push showCursorStr
  IO.print (String.intercalate "" buffer.toList)
  (← IO.getStdout).flush
  return m
end Bliku.Tui

namespace Bliku.Tui
/-- 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
structure Rect where
  row : Nat
  col : Nat
  height : Nat
  width : Nat
  deriving Inhabited
end Bliku.Tui

import Bliku.Tui.Primitives
import Bliku.Tui.Model
import Bliku.Tui.Terminal
namespace Bliku.Tui
open Bliku.Tui.Terminal
def shouldRenderMessageAsFloat (msg : String) : Bool :=
  let m := msg.trimAscii.toString
  if m.isEmpty then
    false
  else
    m.startsWith "Error" ||
    m.startsWith "Cannot" ||
    m.startsWith "Invalid" ||
    m.startsWith "Unknown" ||
    m.startsWith "No " ||
    m.startsWith "Empty " ||
    m.startsWith "Usage:" ||
    m.startsWith "failed" ||
    m.startsWith "Failed" ||
    m.contains "not found"
def renderStatusBar (m : Model) : String :=
  let plain := m.message.trimAscii.toString
  let floatMsg := shouldRenderMessageAsFloat plain
  match m.mode with
  | .command => s!":{m.commandBuffer}"
  | .searchForward => s!"/{m.commandBuffer}"
  | .searchBackward => s!"?{m.commandBuffer}"
  | _ => if floatMsg then "" else plain
structure FloatingOverlayLayout where
  top : Nat
  left : Nat
  innerWidth : Nat
  titleRows : Nat
  contentRows : Nat
  deriving Inhabited
def computeFloatingOverlayLayout (rows cols : Nat) (overlay : FloatingOverlay) : Option FloatingOverlayLayout := Id.run do
  let availableRows := if rows > 1 then rows - 1 else rows
  if cols < 8 || availableRows < 4 then
    return none
  let lines := if overlay.lines.isEmpty then #[""] else overlay.lines
  let titleText := if overlay.title.isEmpty then "" else s!"[{overlay.title}]"
  let titleRows := if titleText.isEmpty then 0 else 1
  let naturalWidthContent := lines.foldl (fun acc ln => max acc ln.length) 0
  let naturalWidth := max naturalWidthContent titleText.length
  let maxInnerWidth := if cols > 8 then cols - 8 else 1
  let targetWidth := if overlay.maxWidth > 0 then overlay.maxWidth else naturalWidth
  let innerWidth := max 1 (min targetWidth maxInnerWidth)
  let maxContentRows := if availableRows > titleRows + 2 then availableRows - titleRows - 2 else 0
  if maxContentRows == 0 then return none
  let contentRows := max 1 (min lines.size maxContentRows)
  let boxHeight := contentRows + titleRows + 2
  let boxWidth := innerWidth + 4
  let top := (availableRows - boxHeight) / 2
  let left := (cols - boxWidth) / 2
  return some { top, left, innerWidth, titleRows, contentRows }
def renderFloatingOverlay (rows cols : Nat) (overlay : FloatingOverlay) : Array String := Id.run do
  let some layout := computeFloatingOverlayLayout rows cols overlay | return #[]
  let lines := if overlay.lines.isEmpty then #[""] else overlay.lines
  let titleText := if overlay.title.isEmpty then "" else s!"[{overlay.title}]"
  let border := "+" ++ "".pushn '-' (layout.innerWidth + 2) ++ "+"
  let mut out : Array String := #[]
  out := out.push (moveCursorStr layout.top layout.left)
  out := out.push border
  if layout.titleRows == 1 then
    out := out.push (moveCursorStr (layout.top + 1) layout.left)
    let clipped := (titleText.take layout.innerWidth).toString
    let pad := if clipped.length < layout.innerWidth then "".pushn ' ' (layout.innerWidth - clipped.length) else ""
    out := out.push s!"| {clipped}{pad} |"
  for i in [0:layout.contentRows] do
    let raw := lines[i]?.getD ""
    let clipped := (raw.take layout.innerWidth).toString
    let pad := if clipped.length < layout.innerWidth then "".pushn ' ' (layout.innerWidth - clipped.length) else ""
    let row := layout.top + 1 + layout.titleRows + i
    out := out.push (moveCursorStr row layout.left)
    out := out.push s!"| {clipped}{pad} |"
  out := out.push (moveCursorStr (layout.top + layout.contentRows + layout.titleRows + 1) layout.left)
  out := out.push border
  out
def messageOverlayForState (m : Model) : Option FloatingOverlay :=
  let plain := m.message.trimAscii.toString
  let floatMsg := shouldRenderMessageAsFloat plain
  if m.floatingOverlay.isNone && m.mode != .command && m.mode != .searchForward && m.mode != .searchBackward && floatMsg then
    if plain.isEmpty then none
    else some { title := "Message", lines := (plain.splitOn "\n").toArray }
  else
    none
def renderCompletionPopup (_rows cols : Nat) (m : Model) (cursorPos : Option (Nat × Nat)) : Array String := Id.run do
  let some popup := m.completionPopup | return #[]
  let some (cursorRow, cursorCol) := cursorPos | return #[]
  if popup.items.isEmpty then return #[]
  let visibleMax := min 8 popup.items.size
  let labels := popup.items.extract 0 visibleMax |>.map (fun it => it.label)
  let naturalW := labels.foldl (fun acc s => max acc s.length) 0
  let innerWidth := max 8 (min 48 naturalW)
  let boxWidth := innerWidth + 2
  let top := cursorRow + 1
  let left := if cursorCol + boxWidth < cols then cursorCol else (cols - boxWidth)
  let borderCh := if m.config.hSplitStr.isEmpty then '-' else m.config.hSplitStr.toList[0]!
  let hline := "".pushn borderCh innerWidth
  let border := m.config.vSplitStr ++ hline ++ m.config.vSplitStr
  let mut out : Array String := #[]
  out := out.push (moveCursorStr top left)
  out := out.push border
  let selected := if popup.selected < visibleMax then popup.selected else 0
  for i in [0:visibleMax] do
    let label := (labels[i]!.take innerWidth).toString
    let pad := if label.length < innerWidth then "".pushn ' ' (innerWidth - label.length) else ""
    out := out.push (moveCursorStr (top + 1 + i) left)
    out := out.push m.config.vSplitStr
    if i == selected then
      out := out.push "\x1b[7m"
      out := out.push label
      out := out.push pad
      out := out.push m.config.resetStyle
    else
      out := out.push label
      out := out.push pad
    out := out.push m.config.vSplitStr
  out := out.push (moveCursorStr (top + visibleMax + 1) left)
  out := out.push border
  out
end Bliku.Tui

import Bliku.Tui.Window
namespace Bliku.Tui
inductive Mode where
  | normal
  | insert
  | command
  | searchForward
  | searchBackward
  | visual
  | visualBlock
  deriving Repr, BEq, Inhabited
instance : ToString Mode where
  toString
    | .normal => "NORMAL"
    | .insert => "INSERT"
    | .command => "COMMAND"
    | .searchForward => "SEARCH"
    | .searchBackward => "SEARCH"
    | .visual => "VISUAL"
    | .visualBlock => "VISUAL BLOCK"
structure BufferState where
  id : Nat
  filename : Option String
  lines : Array String
  missingEol : Bool := false
  deriving Inhabited
structure FloatingOverlay where
  title : String
  lines : Array String
  maxWidth : Nat := 0
  cursorRow : Nat := 0
  cursorCol : Nat := 0
  deriving Repr, Inhabited
structure CompletionItem where
  label : String
  insertText : String
  deriving Repr, Inhabited
structure CompletionPopup where
  items : Array CompletionItem
  selected : Nat := 0
  anchorRow : Nat
  anchorCol : Nat
  deriving Repr, Inhabited
structure UiConfig where
  showLineNumbers : Bool := true
  vSplitStr : String := "│"
  hSplitStr : String := "─"
  emptyLineMarker : String := "~"
  statusBarStyle : String := ""
  resetStyle : String := "\x1b[0m"
  searchHighlightStyle : String := ""
  searchHighlightCursorStyle : String := ""
  visualSelectionStyle : String := "\x1b[7m"
  cursorCharStyle : String := "\x1b[47m\x1b[30m"
  cursorSpaceStyle : String := "\x1b[47m\x1b[30m"
  tabStop : Nat := 4
  deriving Inhabited
structure Model where
  mode : Mode
  workgroupName : String
  workspace : WorkspaceView
  buffers : Array BufferState
  selectionStart : Option Cursor := none
  message : String
  commandBuffer : String
  floatingOverlay : Option FloatingOverlay := none
  completionPopup : Option CompletionPopup := none
  config : UiConfig := {}
  windowHeight : Nat := 24
  windowWidth : Nat := 80
  dirty : Bool := true
  deriving Inhabited
def getBuffer (m : Model) (id : Nat) : BufferState :=
  m.buffers.find? (fun b => b.id == id) |>.getD { id := id, filename := none, lines := #[] }
end Bliku.Tui