layout := .window 0 { bufferId := 0, cursor := { row := 0, col := 0 }, scrollRow := 0, scrollCol := 0 }
    activeWindowId := 0

    desktop := {
      layout := .pane 0 { contentId := 0, cursor := { row := 0, col := 0 }, scrollRow := 0, scrollCol := 0 }
      activePaneId := 0
    }

private def mkModel (mode : Mode := .normal) (selectionStart : Option Cursor := none) : Model :=

private def mkModel : Model :=

    mode := mode
    workgroupName := "wg"

    selectionStart := selectionStart
    message := ""
    commandBuffer := ""

  let rendered := renderVisibleLine (mkModel) buf 0 0 0 4 (some { row := 1, col := 0 })

  let rendered := renderVisibleLine mkModel {} buf 0 0 0 4 (some { row := 1, col := 0 })

  let rendered := renderVisibleLine (mkModel) buf 0 0 0 20 none

  let rendered := renderVisibleLine mkModel {} buf 0 0 0 20 none

  let model := mkModel .visual (some { row := 0, col := 0 })

  let input : RenderInput := {
    selection := some { anchor := { row := 0, col := 0 }, cursor := { row := 0, col := 1 } }
  }

  let rendered := renderVisibleLine model buf 0 0 0 3 (some { row := 0, col := 1 })

  let rendered := renderVisibleLine mkModel input buf 0 0 0 3 (some { row := 0, col := 1 })

private def floatingClusterLayoutTest : IO Unit := do
  let layout : Bliku.PaneLayout :=
    .hsplit
      (.pane 0 { contentId := 0, cursor := { row := 0, col := 0 }, scrollRow := 0, scrollCol := 0 })
      (.group 100 <|
        .vsplit
          (.pane 1 { contentId := 1, cursor := { row := 0, col := 0 }, scrollRow := 0, scrollCol := 0 })
          (.pane 2 { contentId := 2, cursor := { row := 0, col := 0 }, scrollRow := 0, scrollCol := 0 })
          0.5)
      0.5
  let desktop : Bliku.DesktopLayout := {
    layout := layout
    activePaneId := 2
    floating := {
      clusters := #[{ root := .group 100, rowOffset := 1, colOffset := 2 }]
    }
  }
  let ws : WorkspaceView := { name := "test", desktop := desktop }
  assertEq "floating-cluster-pane-1" (ws.isFloatingWindow 1) true
  assertEq "floating-cluster-pane-2" (ws.isFloatingWindow 2) true
  assertEq "floating-cluster-pane-0" (ws.isFloatingWindow 0) false
  let extracted := layout.extractFloatingRoot (.group 100) |>.map Bliku.PaneLayout.getPaneIds
  assertEq "floating-cluster-extract" extracted (some [1, 2])
  let removed := layout.removeFloatingRoot (.group 100) |>.map Bliku.PaneLayout.getPaneIds
  assertEq "floating-cluster-remove" removed (some [0])
private def floatingSizePolicyTest : IO Unit := do
  let defaultBounds :=
    Bliku.computeFloatingClusterBounds 50 160 0 { root := .pane 1, sizePolicy := .default }
  let multiBounds :=
    Bliku.computeFloatingClusterBounds 50 160 0 { root := .group 100, sizePolicy := .multiPane }
  let customBounds :=
    Bliku.computeFloatingClusterBounds 50 160 0 {
      root := .group 200
      sizePolicy := .custom {
        width := .fixed 120
        height := .ratio 0.5
        minWidth := some 80
        maxHeight := some 30
      }
    }
  let some (_, _, defaultH, defaultW) := defaultBounds
    | throw <| IO.userError "default bounds missing"
  let some (_, _, multiH, multiW) := multiBounds
    | throw <| IO.userError "multi bounds missing"
  let some (_, _, customH, customW) := customBounds
    | throw <| IO.userError "custom bounds missing"
  assertEq "floating-size-multipane-wider" (decide (multiW > defaultW)) true
  assertEq "floating-size-multipane-taller" (decide (multiH > defaultH)) true
  assertEq "floating-size-custom-width" customW 120
  assertEq "floating-size-custom-height" customH 24
private def floatingChromeBoxTest : IO Unit := do
  let box := Bliku.Widget.renderFloatingChromeBox
    { kind := .bordered, title := some "Explorer" }
    16 4
    "[A]" "[I]" "[/]"
    true
  assertEq "floating-chrome-line-count" box.lines.size 4
  assertEq "floating-chrome-inset-top" box.insetTop 1
  assertEq "floating-chrome-inset-left" box.insetLeft 1
  assertEq "floating-chrome-top-line" box.lines[0]! "[A]┌ Explorer ────┐[/]"
private def rectSafeLineRenderTest : IO Unit := do
  let buf : BufferState := {
    id := 0
    filename := none
    lines := #["abc"]
  }
  let rendered := renderVisibleLineInRect mkModel {} buf 0 0 0 5 none
  assertEq "rect-safe-line-render" rendered "abc  "
  assertEq "rect-safe-line-no-clear" (rendered.contains '\x1b' && rendered.contains 'K') false
private def eofMarkerPlacementTest : IO Unit := do
  let marker := renderEmptyLineMarkerInRect { emptyLineMarker := "・" } 6
  assertEq "eof-marker-placement" marker "・    "

  floatingClusterLayoutTest
  floatingSizePolicyTest
  floatingChromeBoxTest
  rectSafeLineRenderTest
  eofMarkerPlacementTest

import Bliku.Style
import Bliku.Decoration
import Bliku.Layout
import Bliku.Widget.TextView
import Bliku.Widget.Prompt
import Bliku.Widget.List
import Bliku.Widget.Popup
import Bliku.Widget.Chrome

import Bliku.Decoration
namespace Bliku.Widget
open Bliku
structure TextViewProps where
  lines : Array String
  scrollCol : Nat := 0
  byteDecorations : Array ByteDecoration := #[]
  cellDecorations : Array CellDecoration := #[]
  cursor : Option CursorDecoration := none
  resetStyle : String := "\x1b[0m"
  deriving Inhabited
structure VisibleCell where
  text : String
  col : Nat
  startByte : Nat
  endByte : Nat
  deriving Repr, Inhabited
private def collectVisibleCells (line : String) (scrollCol width : Nat) : Array VisibleCell := Id.run do
  let mut out : Array VisibleCell := #[]
  let mut bytePos := 0
  let mut col := 0
  for ch in line.toList do
    let nextByte := bytePos + ch.utf8Size
    if scrollCol <= col && col < scrollCol + width then
      out := out.push {
        text := ch.toString
        col := col
        startByte := bytePos
        endByte := nextByte
      }
    bytePos := nextByte
    col := col + 1
  out
private def lineDisplayLength (line : String) : Nat :=
  line.toList.length
private def faceForByteRange
    (decos : Array ByteDecoration) (row byteStart byteEnd : Nat) : Option String :=
  let rec loop (i : Nat) (best : Option ByteDecoration) : Option String :=
    if i >= decos.size then
      best.map ByteDecoration.style
    else
      let deco := decos[i]!
      let best' :=
        if deco.row == row && byteStart < deco.endByte && byteEnd > deco.startByte then
          match best with
          | none => some deco
          | some current => if current.priority <= deco.priority then some deco else best
        else
          best
      loop (i + 1) best'
  loop 0 none
private def faceForCell
    (decos : Array CellDecoration) (row col : Nat) : Option String :=
  let rec loop (i : Nat) (best : Option CellDecoration) : Option String :=
    if i >= decos.size then
      best.map CellDecoration.style
    else
      let deco := decos[i]!
      let best' :=
        if deco.row == row && deco.startCol <= col && col < deco.endCol then
          match best with
          | none => some deco
          | some current => if current.priority <= deco.priority then some deco else best
        else
          best
      loop (i + 1) best'
  loop 0 none
def renderVisibleLine (props : TextViewProps) (row width : Nat) : String := Id.run do
  let line := props.lines[row]?.getD ""
  let visibleCells := collectVisibleCells line props.scrollCol width
  let mut out : Array String := #[]
  let mut activeStyle : Option String := none
  for cell in visibleCells do
    let desiredStyle : Option String :=
      match props.cursor with
      | some cur =>
          if cur.row == row && cur.col == cell.col then
            some (if cell.text == " " then cur.spaceStyle else cur.charStyle)
          else
            (faceForCell props.cellDecorations row cell.col).orElse
              (fun _ => faceForByteRange props.byteDecorations row cell.startByte cell.endByte)
      | none =>
          (faceForCell props.cellDecorations row cell.col).orElse
            (fun _ => faceForByteRange props.byteDecorations row cell.startByte cell.endByte)
    if desiredStyle != activeStyle then
      match activeStyle with
      | some _ => out := out.push props.resetStyle
      | none => pure ()
      match desiredStyle with
      | some style => out := out.push style
      | none => pure ()
      activeStyle := desiredStyle
    out := out.push cell.text
  if activeStyle.isSome then
    out := out.push props.resetStyle
  return String.intercalate "" out.toList
def appendCursorOnBlankCell (props : TextViewProps) (row width : Nat) (lineToDraw : String) : String := Id.run do
  let some cur := props.cursor | return lineToDraw
  if cur.row != row || cur.col < props.scrollCol then
    return lineToDraw
  let line := props.lines[row]?.getD ""
  let visCol := cur.col - props.scrollCol
  let visLen := min width (lineDisplayLength line - props.scrollCol)
  if visCol < visLen || visCol >= width then
    return lineToDraw
  let padCount := visCol - visLen
  return lineToDraw ++ ("".pushn ' ' padCount) ++ cur.spaceStyle ++ " " ++ props.resetStyle
end Bliku.Widget

namespace Bliku.Widget
structure PromptProps where
  leader : String := ""
  text : String := ""
  cursorCol : Nat := 0
  deriving Repr, Inhabited
def renderPrompt (props : PromptProps) : String :=
  props.leader ++ props.text
def promptCursorCol (props : PromptProps) : Nat :=
  props.leader.length + props.cursorCol
end Bliku.Widget

namespace Bliku.Widget
structure PopupProps where
  title : String := ""
  lines : Array String := #[]
  maxWidth : Nat := 0
  borderCorner : String := "+"
  borderHorizontal : Char := '-'
  borderVertical : String := "|"
  deriving Inhabited
structure PopupBox where
  lines : Array String
  innerWidth : Nat
  titleRows : Nat
  contentRows : Nat
  deriving Inhabited
def renderPopupBox (props : PopupProps) : PopupBox := Id.run do
  let lines := if props.lines.isEmpty then #[""] else props.lines
  let titleText := if props.title.isEmpty then "" else s!"[{props.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 innerWidth := max 1 (if props.maxWidth > 0 then min props.maxWidth naturalWidth else naturalWidth)
  let border := props.borderCorner ++ "".pushn props.borderHorizontal (innerWidth + 2) ++ props.borderCorner
  let mut out : Array String := #[border]
  if titleRows == 1 then
    let clipped := (titleText.take innerWidth).toString
    let pad := if clipped.length < innerWidth then "".pushn ' ' (innerWidth - clipped.length) else ""
    out := out.push s!"{props.borderVertical} {clipped}{pad} {props.borderVertical}"
  for raw in lines do
    let clipped := (raw.take innerWidth).toString
    let pad := if clipped.length < innerWidth then "".pushn ' ' (innerWidth - clipped.length) else ""
    out := out.push s!"{props.borderVertical} {clipped}{pad} {props.borderVertical}"
  out := out.push border
  return { lines := out, innerWidth := innerWidth, titleRows := titleRows, contentRows := lines.size }
end Bliku.Widget

namespace Bliku.Widget
structure ListItem where
  label : String
  deriving Repr, Inhabited
structure ListProps where
  items : Array ListItem
  selected : Nat := 0
  maxVisible : Nat := 8
  width : Nat := 0
  borderLeft : String := "|"
  borderRight : String := "|"
  borderFill : Char := '-'
  selectedStyle : String := "\x1b[7m"
  resetStyle : String := "\x1b[0m"
  deriving Inhabited
structure ListBox where
  lines : Array String
  width : Nat
  height : Nat
  deriving Inhabited
def renderListBox (props : ListProps) : ListBox := Id.run do
  if props.items.isEmpty then
    return { lines := #[], width := 0, height := 0 }
  let visibleCount := min props.maxVisible props.items.size
  let labels := props.items.extract 0 visibleCount |>.map ListItem.label
  let naturalW := labels.foldl (fun acc s => max acc s.length) 0
  let innerWidth := max 1 (if props.width == 0 then naturalW else props.width)
  let border := props.borderLeft ++ "".pushn props.borderFill innerWidth ++ props.borderRight
  let selected := if props.selected < visibleCount then props.selected else 0
  let mut out : Array String := #[border]
  for i in [0:visibleCount] do
    let label := (labels[i]!.take innerWidth).toString
    let pad := if label.length < innerWidth then "".pushn ' ' (innerWidth - label.length) else ""
    let body :=
      if i == selected then
        props.selectedStyle ++ label ++ pad ++ props.resetStyle
      else
        label ++ pad
    out := out.push (props.borderLeft ++ body ++ props.borderRight)
  out := out.push border
  return { lines := out, width := innerWidth + props.borderLeft.length + props.borderRight.length, height := out.size }
end Bliku.Widget

import Bliku.Layout
namespace Bliku.Widget
structure ChromeBox where
  lines : Array String
  insetTop : Nat := 0
  insetLeft : Nat := 0
  insetBottom : Nat := 0
  insetRight : Nat := 0
  deriving Inhabited
def renderFloatingChromeBox
    (chrome : Bliku.FloatingChrome)
    (width height : Nat)
    (activeStyle inactiveStyle resetStyle : String)
    (isActive : Bool) : ChromeBox := Id.run do
  if chrome.kind == .none || width < 2 || height < 2 then
    return { lines := #[] }
  let style := if isActive then activeStyle else inactiveStyle
  let title := chrome.title.getD ""
  let topFill := if width > 2 then width - 2 else 0
  let rawTop := if title.isEmpty then "".pushn '─' topFill else
    let core := s!" {title} "
    let clipped := (core.take topFill).toString
    clipped ++ "".pushn '─' (topFill - clipped.length)
  let top := style ++ "┌" ++ rawTop ++ "┐" ++ resetStyle
  let middle := style ++ "│" ++ resetStyle ++ "".pushn ' ' (width - 2) ++ style ++ "│" ++ resetStyle
  let bottom := style ++ "└" ++ "".pushn '─' topFill ++ "┘" ++ resetStyle
  let mut lines : Array String := #[top]
  for _ in [0:height - 2] do
    lines := lines.push middle
  lines := lines.push bottom
  return {
    lines := lines
    insetTop := 1
    insetLeft := 1
    insetBottom := 1
    insetRight := 1
  }
end Bliku.Widget

import Bliku.Tui.RenderInput

import Bliku.Tui.Primitives

import Bliku.Layout

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

abbrev Cursor := Bliku.Cursor
abbrev ViewState := Bliku.PaneView
abbrev Layout := Bliku.PaneLayout

inductive Layout where
  | window (id : Nat) (view : ViewState)
  | hsplit (left right : Layout) (ratio : Float)
  | vsplit (top bottom : Layout) (ratio : Float)
  deriving Repr, Inhabited

def ViewState.bufferId (view : ViewState) : Nat :=
  view.contentId

  layout : Layout
  activeWindowId : Nat
  floatingWindows : List Nat := []
  floatingWindowOffsets : List (Nat × Int × Int) := []

  desktop : Bliku.DesktopLayout

def WorkspaceView.layout (ws : WorkspaceView) : Layout :=
  ws.desktop.layout
def WorkspaceView.activeWindowId (ws : WorkspaceView) : Nat :=
  ws.desktop.activePaneId

def WorkspaceView.floatingWindows (ws : WorkspaceView) : List Nat :=
  (ws.desktop.floating.getClusters ws.layout).foldl
    (fun acc cluster =>
      match ws.layout.extractFloatingRoot cluster.root with
      | some subtree => acc ++ subtree.getPaneIds
      | none => acc)
    []
def WorkspaceView.floatingWindowOffsets (ws : WorkspaceView) : List (Nat × Int × Int) :=
  (ws.desktop.floating.getClusters ws.layout).foldl
    (fun acc cluster =>
      match cluster.root with
      | .pane wid => (wid, cluster.rowOffset, cluster.colOffset) :: acc
      | .group _ => acc)
    []
def WorkspaceView.floatingClusters (ws : WorkspaceView) : Array Bliku.FloatingCluster :=
  ws.desktop.floating.getClusters ws.layout

  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)

  Bliku.PaneLayout.findView l id

  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

  Bliku.PaneLayout.updateView l id f

  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

  l.getPaneIds.contains windowId

  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)

  Bliku.PaneLayout.remove l id

  match l with
  | .window id _ => [id]
  | .hsplit left right _ => getWindowIds left ++ getWindowIds right
  | .vsplit top bottom _ => getWindowIds top ++ getWindowIds bottom

  l.getPaneIds

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

  l.getAllPaneBounds h w

  ws.floatingWindows.contains windowId

  ws.desktop.floating.clusterForPane? ws.layout windowId |>.isSome

  ws.floatingWindows.foldl (fun acc wid =>
    match ws.layout.findView wid with
    | some _ => acc.push wid

  ws.floatingClusters.foldl (fun acc cluster =>
    match ws.layout.extractFloatingRoot cluster.root with
    | some subtree => acc ++ subtree.getPaneIds.toArray

  let ids := ws.getFloatingWindowIds

  let clusters := ws.floatingClusters

    if i >= ids.size then none
    else if ids[i]! == windowId then some i
    else loop (i + 1)

    if i >= clusters.size then
      none
    else
      match ws.layout.extractFloatingRoot clusters[i]!.root with
      | some subtree =>
          if subtree.getPaneIds.contains windowId then some i else loop (i + 1)
      | none => loop (i + 1)

  match ws.floatingWindowOffsets.find? (fun (wid, _, _) => wid == windowId) with
  | some (_, ro, co) => (ro, co)

  match ws.desktop.floating.clusterForPane? ws.layout windowId with
  | some cluster => (cluster.rowOffset, cluster.colOffset)

  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)

  Bliku.computeFloatingClusterBounds rows cols idx { root := .pane idx }
def computeFloatingClusterBounds (rows cols idx : Nat) (cluster : Bliku.FloatingCluster) : Option (Nat × Nat × Nat × Nat) :=
  Bliku.computeFloatingClusterBounds rows cols idx cluster

    match computeFloatingWindowBounds windowHeight windowWidth idx with

    match ws.desktop.floating.clusterForPane? ws.layout windowId with

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

    | some cluster =>
      match computeFloatingClusterBounds windowHeight windowWidth idx cluster with
      | none => none
      | some (top, left, h, w) =>
        let (rowOff, colOff) := (cluster.rowOffset, cluster.colOffset)
        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)

import Bliku.Style

inductive Color where
  | ansi (code : Nat)
  | rgb (r g b : Nat)
  deriving Repr, BEq, Inhabited
structure Face where
  fg : Option Color := none
  bg : Option Color := none
  bold : Bool := false
  italic : Bool := false
  underline : Bool := false
  deriving Repr, BEq, Inhabited

abbrev Color := Bliku.Color
abbrev Face := Bliku.Face

private def colorToAnsi (channel : String) : Color → String
  | .ansi code => s!"\x1b[{channel};5;{code}m"
  | .rgb r g b => s!"\x1b[{channel};2;{r};{g};{b}m"
def Face.toAnsi (face : Face) : String := Id.run do
  let mut parts : Array String := #[]
  match face.fg with
  | some color => parts := parts.push (colorToAnsi "38" color)
  | none => pure ()
  match face.bg with
  | some color => parts := parts.push (colorToAnsi "48" color)
  | none => pure ()
  if face.bold then
    parts := parts.push "\x1b[1m"
  if face.italic then
    parts := parts.push "\x1b[3m"
  if face.underline then
    parts := parts.push "\x1b[4m"
  return String.intercalate "" parts.toList

import Bliku.Tui.Window
import Bliku.Tui.Model
namespace Bliku.Tui
structure SelectionState where
  anchor : Cursor
  cursor : Cursor
  block : Bool := false
  deriving Repr, Inhabited
structure CommandLineState where
  leader : String
  text : String
  cursorCol : Nat := 0
  deriving Repr, Inhabited
structure OverlayView where
  title : String
  lines : Array String
  maxWidth : Nat := 0
  cursorRow : Nat := 0
  cursorCol : Nat := 0
  deriving Repr, Inhabited
structure CompletionView where
  items : Array CompletionItem
  selected : Nat := 0
  anchorRow : Nat
  anchorCol : Nat
  deriving Repr, Inhabited
structure WindowChrome where
  statusLine : String := ""
  deriving Repr, Inhabited
structure RenderInput where
  selection : Option SelectionState := none
  commandLine : Option CommandLineState := none
  messageLine : String := ""
  statusLine : String := ""
  overlay : Option OverlayView := none
  completion : Option CompletionView := none
  hideTerminalCursor : Bool := false
  deriving Inhabited
end Bliku.Tui

import Bliku.Tui.RenderInput

import Bliku.Decoration
import Bliku.Widget.TextView
import Bliku.Widget.Chrome

structure VisibleCell where
  text : String
  col : Nat
  startByte : Nat
  endByte : Nat
  deriving Repr, Inhabited

private def getBufferLine (buf : BufferState) (row : Nat) : String :=
  buf.lines[row]?.getD ""

private def collectVisibleCells (line : String) (scrollCol width : Nat) : Array VisibleCell := Id.run do
  let mut out : Array VisibleCell := #[]
  let mut bytePos := 0
  let mut col := 0
  for ch in line.toList do
    let nextByte := bytePos + ch.utf8Size
    if scrollCol <= col && col < scrollCol + width then
      out := out.push {
        text := ch.toString
        col := col
        startByte := bytePos
        endByte := nextByte
      }
    bytePos := nextByte
    col := col + 1

private def charDisplayWidth (ch : Char) : Nat :=
  let n := ch.toNat
  if
    (0x1100 <= n && n <= 0x115F) ||
    (0x2329 <= n && n <= 0x232A) ||
    (0x2E80 <= n && n <= 0xA4CF) ||
    (0xAC00 <= n && n <= 0xD7A3) ||
    (0xF900 <= n && n <= 0xFAFF) ||
    (0xFE10 <= n && n <= 0xFE19) ||
    (0xFE30 <= n && n <= 0xFE6F) ||
    (0xFF00 <= n && n <= 0xFF60) ||
    (0xFFE0 <= n && n <= 0xFFE6)
  then 2 else 1
private def lineDisplayLength (line : String) : Nat :=
  line.toList.foldl (fun acc ch => acc + charDisplayWidth ch) 0
private def takeDisplayWidth (s : String) (width : Nat) : String := Id.run do
  let mut out := ""
  let mut used := 0
  for ch in s.toList do
    let chWidth := charDisplayWidth ch
    if used + chWidth <= width then
      out := out.push ch
      used := used + chWidth

private def lineDisplayLength (line : String) : Nat :=
  line.toList.length

private def padPlainLine (s : String) (width : Nat) : String :=
  let clipped := takeDisplayWidth s width
  let clippedWidth := lineDisplayLength clipped
  let pad := if clippedWidth < width then "".pushn ' ' (width - clippedWidth) else ""
  clipped ++ pad

private def getBufferLine (buf : BufferState) (row : Nat) : String :=
  buf.lines[row]?.getD ""

def renderEmptyLineMarkerInRect (config : UiConfig) (width : Nat) : String :=
  padPlainLine config.emptyLineMarker width
private def renderedWindowLineWidth
    (line : String) (scrollCol availableWidth : Nat) (windowCursor : Option Cursor) : Nat :=
  let lineLen := lineDisplayLength line
  let visibleLen := if lineLen > scrollCol then min availableWidth (lineLen - scrollCol) else 0
  match windowCursor with
  | some cur =>
      if cur.col >= scrollCol then
        let visCol := cur.col - scrollCol
        if visibleLen <= visCol && visCol < availableWidth then
          visCol + 1
        else
          visibleLen
      else
        visibleLen
  | none => visibleLen

private def isVisualMode (mode : Mode) : Bool :=
  mode == .visual || mode == .visualBlock

private def byteDecorationsForLine (m : Model) (buf : BufferState) (lineIdx : Nat) (line : String) : Array ByteDecoration :=
  let palette := syntaxPaletteFor m buf
  (syntaxSpansForLine buf lineIdx line).foldl (fun acc span =>
    match Syntax.Palette.faceFor palette span.kind with
    | some face =>
        acc.push {
          row := lineIdx
          startByte := span.startByte
          endByte := span.endByte
          priority := 10
          style := face.toAnsi
        }
            | none => acc) #[]

private def isInSelection (m : Model) (cur : Cursor) (row col : Nat) : Bool :=
  if !isVisualMode m.mode then
    false

private def isInSelection (selection : SelectionState) (row col : Nat) : Bool :=
  if selection.block then
    let minRow := min selection.anchor.row selection.cursor.row
    let maxRow := max selection.anchor.row selection.cursor.row
    let minCol := min selection.anchor.col selection.cursor.col
    let maxCol := max selection.anchor.col selection.cursor.col
    row >= minRow && row <= maxRow && col >= minCol && col <= maxCol

    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

    let (p1, p2) := normalizeCursorRange selection.anchor selection.cursor
    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 selectionDecorationsForLine
    (config : UiConfig) (selection : Option SelectionState) (lineIdx scrollCol availableWidth : Nat) : Array CellDecoration := Id.run do
  let some selection := selection | return #[]
  let mut startCol : Option Nat := none
  let mut endCol := scrollCol
  for col in [scrollCol:scrollCol + availableWidth] do
    if isInSelection selection lineIdx col then
      if startCol.isNone then
        startCol := some col
      endCol := col + 1
  match startCol with
  | some start =>
      #[{
        row := lineIdx
        startCol := start
        endCol := endCol
        priority := 100
        style := config.visualSelectionStyle
      }]
  | none => #[]
private def cursorDecorationForLine
    (m : Model) (windowId lineIdx : Nat) (windowCursor : Option Cursor) : Option CursorDecoration :=
  match windowCursor with
  | some cur =>
      if windowId == m.workspace.activeWindowId && lineIdx == cur.row then
        some {
          row := lineIdx
          col := cur.col
          charStyle := m.config.cursorCharStyle
          spaceStyle := m.config.cursorSpaceStyle
        }

        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

        none
  | none => none

    (m : Model) (buf : BufferState) (windowId lineIdx scrollCol availableWidth : Nat)
    (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 }

    (m : Model) (input : RenderInput) (buf : BufferState) (windowId lineIdx scrollCol availableWidth : Nat)
    (windowCursor : Option Cursor) : String :=

  let visibleCells := collectVisibleCells line scrollCol availableWidth
  let syntaxSpans := syntaxSpansForLine buf lineIdx line
  let syntaxPalette := syntaxPaletteFor m buf
  let mut out : Array String := #[]
  let mut activeStyle : Option String := none
  for cell in visibleCells do
    let isCursor :=
      windowCursor.isSome &&
      windowId == m.workspace.activeWindowId &&
      lineIdx == activeRow &&
      cell.col == activeCol
    let desiredStyle : Option String :=
      if isCursor then
        if cell.text == " " then some m.config.cursorSpaceStyle else some m.config.cursorCharStyle
      else if isInSelection m selectionCur lineIdx cell.col then
        some m.config.visualSelectionStyle
      else
        (Syntax.faceForByteRange syntaxPalette syntaxSpans cell.startByte cell.endByte).map Syntax.Face.toAnsi
    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 cell.text
  if activeStyle.isSome then
    out := out.push m.config.resetStyle
  return String.intercalate "" out.toList

  let props : Bliku.Widget.TextViewProps := {
    lines := #[line]
    scrollCol := scrollCol
    byteDecorations := (byteDecorationsForLine m buf lineIdx line).map (fun deco => { deco with row := 0 })
    cellDecorations := (selectionDecorationsForLine m.config input.selection lineIdx scrollCol availableWidth).map (fun deco =>
      { deco with row := 0 })
    cursor := (cursorDecorationForLine m windowId lineIdx windowCursor).map (fun deco => { deco with row := 0 })
    resetStyle := m.config.resetStyle
  }
  let styled := Bliku.Widget.renderVisibleLine props 0 availableWidth
  Bliku.Widget.appendCursorOnBlankCell props 0 availableWidth styled

private def appendCursorOnBlankCell
    (m : Model) (windowId lineIdx scrollCol availableWidth : Nat)
    (line : 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 := lineDisplayLength line - scrollCol |> min availableWidth
  if visCol < visLen || visCol >= availableWidth then
    return lineToDraw
  let padCount := visCol - visLen
  return lineToDraw ++ ("".pushn ' ' padCount) ++ m.config.cursorSpaceStyle ++ " " ++ m.config.resetStyle

def renderVisibleLineInRect
    (m : Model) (input : RenderInput) (buf : BufferState) (windowId lineIdx scrollCol availableWidth : Nat)
    (windowCursor : Option Cursor) : String :=
  let line := getBufferLine buf lineIdx
  let rendered := renderVisibleLine m input buf windowId lineIdx scrollCol availableWidth windowCursor
  let occupied := renderedWindowLineWidth line scrollCol availableWidth windowCursor
  let pad := if occupied < availableWidth then "".pushn ' ' (availableWidth - occupied) else ""
  rendered ++ pad

private def renderWindow (m : Model) (windowId : Nat) (view : ViewState) (rect : Rect) : (Array String × Option (Nat × Nat)) := Id.run do

private def renderWindow (m : Model) (input : RenderInput) (windowId : Nat) (view : ViewState) (rect : Rect) : (Array String × Option (Nat × Nat)) := Id.run do

    let lnWidth := if m.config.showLineNumbers then 4 else 0
    let availableWidth := if w > lnWidth then w - lnWidth else 0

      let lnWidth := if m.config.showLineNumbers then 4 else 0
      let availableWidth := if w > lnWidth then w - lnWidth else 0

      let line := getBufferLine buf lineIdx
      let styled := renderVisibleLine m buf windowId lineIdx view.scrollCol availableWidth windowCursor
      let lineToDraw := appendCursorOnBlankCell m windowId lineIdx view.scrollCol availableWidth line styled windowCursor
      out := out.push lineToDraw

      out := out.push (renderVisibleLineInRect m input buf windowId lineIdx view.scrollCol availableWidth windowCursor)

      out := out.push m.config.emptyLineMarker
    out := out.push clearLineStr

      out := out.push (renderEmptyLineMarkerInRect m.config w)

  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 statusStr
  out := out.push clearLineStr

  out := out.push (padPlainLine input.statusLine w)

private def renderLayout (m : Model) (l : Layout) (r c h w : Nat) : (Array String × Option (Nat × Nat)) := Id.run do

private def renderLayout (m : Model) (input : RenderInput) (l : Layout) (r c h w : Nat) (skipFloating : Bool := true) : (Array String × Option (Nat × Nat)) := Id.run do

  | .window id view =>
    if m.workspace.isFloatingWindow id then

  | .group _ body =>
    return renderLayout m input body r c h w skipFloating
  | .pane id view =>
    if skipFloating && m.workspace.isFloatingWindow id then

    let (buf, cur) := renderWindow m id view { row := r, col := c, height := h, width := w }

    let (buf, cur) := renderWindow m input id view { row := r, col := c, height := h, width := w }

    let (leftBuf, leftCur) := renderLayout m left r c h leftW

    let (leftBuf, leftCur) := renderLayout m input left r c h leftW skipFloating

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

    let (rightBuf, rightCur) := renderLayout m input right r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0) skipFloating

    let (topBuf, topCur) := renderLayout m top r c topH w

    let (topBuf, topCur) := renderLayout m input top r c topH w skipFloating

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

    let (bottomBuf, bottomCur) := renderLayout m input bottom (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w skipFloating

private def renderFloatingWindows (m : Model) : (Array String × Option (Nat × Nat)) := Id.run do

private def renderFloatingClusters (m : Model) (input : RenderInput) : (Array String × Option (Nat × Nat)) := Id.run do

  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

  let clusters := ws.floatingClusters
  for i in [0:clusters.size] do
    let cluster := clusters[i]!
    match ws.layout.extractFloatingRoot cluster.root,
      computeFloatingClusterBounds m.windowHeight m.windowWidth i cluster with
    | some subtree, some (baseTop, baseLeft, h, w) =>
      let toNatNonNeg (v : Int) := if v < 0 then 0 else Int.toNat v
      let availableRows := if m.windowHeight > 1 then m.windowHeight - 1 else m.windowHeight
      let maxTop := if availableRows > h then availableRows - h else 0
      let maxLeft := if m.windowWidth > w then m.windowWidth - w else 0
      let top := min maxTop (toNatNonNeg (Int.ofNat baseTop + cluster.rowOffset))
      let left := min maxLeft (toNatNonNeg (Int.ofNat baseLeft + cluster.colOffset))
      let isActive := subtree.getPaneIds.contains ws.activeWindowId
      let chromeBox := Bliku.Widget.renderFloatingChromeBox
        cluster.chrome w h
        m.config.floatingChromeActiveStyle
        m.config.floatingChromeInactiveStyle
        m.config.resetStyle
        isActive
      if !chromeBox.lines.isEmpty then
        for j in [0:chromeBox.lines.size] do
          out := out.push (moveCursorStr (top + j) left)
          out := out.push chromeBox.lines[j]!
      let innerTop := top + chromeBox.insetTop
      let innerLeft := left + chromeBox.insetLeft
      let innerH := h - chromeBox.insetTop - chromeBox.insetBottom
      let innerW := w - chromeBox.insetLeft - chromeBox.insetRight
      if innerH > 0 && innerW > 0 then
        let (buf, cur) := renderLayout m input subtree innerTop innerLeft innerH innerW false
        out := out ++ buf
        if isActive then
          activeCur := cur

private def findOverlayCursorPos (rows cols : Nat) (m : Model) : Option (Nat × Nat) :=
  match m.floatingOverlay with

private def findOverlayCursorPos (rows cols : Nat) (input : RenderInput) : Option (Nat × Nat) :=
  match input.overlay with

def render (model : Model) : IO Model := do

def renderWith (model : Model) (input : RenderInput) : IO Model := do

    m.workspace.getFloatingWindowIds.foldl (fun acc wid =>

    m.workspace.floatingClusters.foldl (fun acc cluster =>

      | some l => l.remove wid

      | some l => l.removeFloatingRoot cluster.root

    | some l => renderLayout m l 0 0 layoutH cols

    | some l => renderLayout m input l 0 0 layoutH cols true

  let (floatBuf, floatCur) := renderFloatingWindows m

  let (floatBuf, floatCur) := renderFloatingClusters m input

  buffer := buffer.push (renderStatusBar m)
  buffer := buffer.push clearLineStr

  buffer := buffer.push (padPlainLine (renderStatusBar input) cols)

  let overlayToRender := m.floatingOverlay.orElse (fun _ => messageOverlayForState m)

  let overlayToRender := input.overlay.orElse (fun _ => messageOverlayForState input)

  buffer := buffer ++ renderCompletionPopup rows cols m activeCur

  if let some popup := input.completion then
    buffer := buffer ++ renderCompletionPopup rows cols m.config popup activeCur

  let overlayCur := findOverlayCursorPos rows cols m

  let overlayCur := findOverlayCursorPos rows cols input

    if m.floatingOverlay.isSome && m.mode != .command && m.mode != .searchForward && m.mode != .searchBackward then

    if input.overlay.isSome && input.commandLine.isNone then

  if m.mode == .command || m.mode == .searchForward || m.mode == .searchBackward then
    buffer := buffer.push (moveCursorStr (rows - 1) (1 + m.commandBuffer.length))

  if let some prompt := input.commandLine then
    buffer := buffer.push (moveCursorStr (rows - 1) (Bliku.Widget.promptCursorCol { leader := prompt.leader, text := prompt.text, cursorCol := prompt.cursorCol }))

  if m.mode == .visual || m.mode == .visualBlock then

  if input.hideTerminalCursor then

def render (model : Model) : IO Model :=
  renderWith model {}

import Bliku.Tui.RenderInput

import Bliku.Widget.Popup
import Bliku.Widget.List
import Bliku.Widget.Prompt

def renderStatusBar (m : Model) : String :=
  let plain := m.message.trimAscii.toString

def renderStatusBar (input : RenderInput) : String :=
  let plain := input.messageLine.trimAscii.toString

  match m.mode with
  | .command => s!":{m.commandBuffer}"
  | .searchForward => s!"/{m.commandBuffer}"
  | .searchBackward => s!"?{m.commandBuffer}"
  | _ => if floatMsg then "" else plain

  match input.commandLine with
  | some cmd => Bliku.Widget.renderPrompt { leader := cmd.leader, text := cmd.text, cursorCol := cmd.cursorCol }
  | none => if floatMsg then input.statusLine else plain

def computeFloatingOverlayLayout (rows cols : Nat) (overlay : FloatingOverlay) : Option FloatingOverlayLayout := Id.run do

def computeFloatingOverlayLayout (rows cols : Nat) (overlay : OverlayView) : Option FloatingOverlayLayout := Id.run do

  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 box := Bliku.Widget.renderPopupBox { title := overlay.title, lines := overlay.lines, maxWidth := overlay.maxWidth }

  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

  let innerWidth := max 1 (min box.innerWidth maxInnerWidth)
  let maxContentRows := if availableRows > box.titleRows + 2 then availableRows - box.titleRows - 2 else 0

  let contentRows := max 1 (min lines.size maxContentRows)
  let boxHeight := contentRows + titleRows + 2

  let contentRows := max 1 (min box.contentRows maxContentRows)
  let boxHeight := contentRows + box.titleRows + 2

  return some { top, left, innerWidth, titleRows, contentRows }

  return some { top, left, innerWidth, titleRows := box.titleRows, contentRows }

def renderFloatingOverlay (rows cols : Nat) (overlay : FloatingOverlay) : Array String := Id.run do

def renderFloatingOverlay (rows cols : Nat) (overlay : OverlayView) : Array String := Id.run do

  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 popup := Bliku.Widget.renderPopupBox { title := overlay.title, lines := overlay.lines, maxWidth := layout.innerWidth }

  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

  for i in [0:popup.lines.size] do
    out := out.push (moveCursorStr (layout.top + i) layout.left)
    out := out.push popup.lines[i]!

def messageOverlayForState (m : Model) : Option FloatingOverlay :=
  let plain := m.message.trimAscii.toString

def messageOverlayForState (input : RenderInput) : Option OverlayView :=
  let plain := input.messageLine.trimAscii.toString

  if m.floatingOverlay.isNone && m.mode != .command && m.mode != .searchForward && m.mode != .searchBackward && floatMsg then

  if input.overlay.isNone && input.commandLine.isNone && floatMsg then

def renderCompletionPopup (_rows cols : Nat) (m : Model) (cursorPos : Option (Nat × Nat)) : Array String := Id.run do
  let some popup := m.completionPopup | return #[]

def renderCompletionPopup (_rows cols : Nat) (config : UiConfig) (popup : CompletionView) (cursorPos : Option (Nat × Nat)) : Array String := Id.run do

  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 items := popup.items.map (fun it => Bliku.Widget.ListItem.mk it.label)
  let borderCh := if config.hSplitStr.isEmpty then '-' else config.hSplitStr.toList[0]!
  let box := Bliku.Widget.renderListBox {
    items := items
    selected := popup.selected
    maxVisible := 8
    borderLeft := config.vSplitStr
    borderRight := config.vSplitStr
    borderFill := borderCh
    selectedStyle := "\x1b[7m"
    resetStyle := config.resetStyle
  }
  if box.lines.isEmpty then
    return #[]

  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 left := if cursorCol + box.width < cols then cursorCol else (cols - box.width)

  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

  for i in [0:box.lines.size] do
    out := out.push (moveCursorStr (top + i) left)
    out := out.push box.lines[i]!

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"

  floatingChromeActiveStyle : String := ""
  floatingChromeInactiveStyle : String := ""

  mode : Mode
  workgroupName : String

  selectionStart : Option Cursor := none
  message : String
  commandBuffer : String
  floatingOverlay : Option FloatingOverlay := none
  completionPopup : Option CompletionPopup := none

namespace Bliku
inductive Color where
  | ansi (code : Nat)
  | rgb (r g b : Nat)
  deriving Repr, BEq, Inhabited
structure Face where
  fg : Option Color := none
  bg : Option Color := none
  bold : Bool := false
  italic : Bool := false
  underline : Bool := false
  deriving Repr, BEq, Inhabited
structure Theme where
  faces : List (String × Face) := []
  deriving Repr, BEq, Inhabited
private def colorToAnsi (channel : String) : Color → String
  | .ansi code => s!"\x1b[{channel};5;{code}m"
  | .rgb r g b => s!"\x1b[{channel};2;{r};{g};{b}m"
def Face.toAnsi (face : Face) : String := Id.run do
  let mut parts : Array String := #[]
  match face.fg with
  | some color => parts := parts.push (colorToAnsi "38" color)
  | none => pure ()
  match face.bg with
  | some color => parts := parts.push (colorToAnsi "48" color)
  | none => pure ()
  if face.bold then
    parts := parts.push "\x1b[1m"
  if face.italic then
    parts := parts.push "\x1b[3m"
  if face.underline then
    parts := parts.push "\x1b[4m"
  return String.intercalate "" parts.toList
end Bliku

namespace Bliku
structure Cursor where
  row : Nat
  col : Nat
  deriving Repr, BEq, Inhabited
structure PaneView where
  contentId : Nat
  cursor : Cursor
  scrollRow : Nat
  scrollCol : Nat
  deriving Repr, Inhabited
inductive FloatingRootRef where
  | pane (id : Nat)
  | group (id : Nat)
  deriving Repr, BEq, Inhabited
inductive FloatingAxisSize where
  | auto
  | fixed (value : Nat)
  | ratio (value : Float)
  deriving Repr, BEq, Inhabited
structure FloatingSizeSpec where
  width : FloatingAxisSize := .auto
  height : FloatingAxisSize := .auto
  minWidth : Option Nat := none
  minHeight : Option Nat := none
  maxWidth : Option Nat := none
  maxHeight : Option Nat := none
  deriving Repr, BEq, Inhabited
inductive FloatingSizePolicy where
  | default
  | multiPane
  | custom (spec : FloatingSizeSpec)
  deriving Repr, BEq, Inhabited
inductive FloatingChromeKind where
  | none
  | bordered
  deriving Repr, BEq, Inhabited
structure FloatingChrome where
  kind : FloatingChromeKind := .none
  title : Option String := none
  deriving Repr, BEq, Inhabited
inductive PaneLayout where
  | pane (id : Nat) (view : PaneView)
  | group (id : Nat) (body : PaneLayout)
  | hsplit (left right : PaneLayout) (ratio : Float)
  | vsplit (top bottom : PaneLayout) (ratio : Float)
  deriving Repr, Inhabited
structure FloatingCluster where
  root : FloatingRootRef
  rowOffset : Int := 0
  colOffset : Int := 0
  sizePolicy : FloatingSizePolicy := .default
  chrome : FloatingChrome := {}
  deriving Repr, BEq, Inhabited
structure FloatingPaneState where
  clusters : Array FloatingCluster := #[]
  deriving Inhabited
structure DesktopLayout where
  layout : PaneLayout
  activePaneId : Nat
  floating : FloatingPaneState := {}
  deriving Inhabited
def PaneLayout.findView (l : PaneLayout) (id : Nat) : Option PaneView :=
  match l with
  | .pane wid v => if wid == id then some v else none
  | .group _ body => body.findView id
  | .hsplit left right _ => (left.findView id).orElse (fun _ => right.findView id)
  | .vsplit top bottom _ => (top.findView id).orElse (fun _ => bottom.findView id)
def PaneLayout.updateView (l : PaneLayout) (id : Nat) (f : PaneView → PaneView) : PaneLayout :=
  let rec go (node : PaneLayout) : PaneLayout × Bool :=
    match node with
    | .pane wid v =>
      if wid == id then (.pane wid (f v), true) else (node, false)
    | .group gid body =>
      let (body', found) := go body
      (.group gid body', found)
    | .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 PaneLayout.remove (l : PaneLayout) (id : Nat) : Option PaneLayout :=
  match l with
  | .pane wid _ => if wid == id then none else some l
  | .group gid body =>
    if gid == id then
      none
    else
      body.remove id |>.map (PaneLayout.group gid)
  | .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 PaneLayout.getPaneIds (l : PaneLayout) : List Nat :=
  match l with
  | .pane id _ => [id]
  | .group _ body => body.getPaneIds
  | .hsplit left right _ => left.getPaneIds ++ right.getPaneIds
  | .vsplit top bottom _ => top.getPaneIds ++ bottom.getPaneIds
def PaneLayout.containsFloatingRoot (l : PaneLayout) (root : FloatingRootRef) : Bool :=
  match l, root with
  | .pane id _, .pane target => id == target
  | .group id _, .group target => id == target
  | .group _ body, root => body.containsFloatingRoot root
  | .hsplit left right _, root => left.containsFloatingRoot root || right.containsFloatingRoot root
  | .vsplit top bottom _, root => top.containsFloatingRoot root || bottom.containsFloatingRoot root
  | _, _ => false
def PaneLayout.extractFloatingRoot (l : PaneLayout) (root : FloatingRootRef) : Option PaneLayout :=
  match l, root with
  | .pane id _, .pane target => if id == target then some l else none
  | .group id _, .group target => if id == target then some l else none
  | .group _ body, root => body.extractFloatingRoot root
  | .hsplit left right _, root => (left.extractFloatingRoot root).orElse (fun _ => right.extractFloatingRoot root)
  | .vsplit top bottom _, root => (top.extractFloatingRoot root).orElse (fun _ => bottom.extractFloatingRoot root)
  | _, _ => none
def PaneLayout.removeFloatingRoot (l : PaneLayout) (root : FloatingRootRef) : Option PaneLayout :=
  match l, root with
  | .pane id _, .pane target => if id == target then none else some l
  | .group id _, .group target => if id == target then none else some l
  | .group gid body, root =>
    body.removeFloatingRoot root |>.map (PaneLayout.group gid)
  | .hsplit left right ratio, root =>
    match left.removeFloatingRoot root with
    | none => some right
    | some left' =>
      match right.removeFloatingRoot root with
      | none => some left'
      | some right' => some (.hsplit left' right' ratio)
  | .vsplit top bottom ratio, root =>
    match top.removeFloatingRoot root with
    | none => some bottom
    | some top' =>
      match bottom.removeFloatingRoot root with
      | none => some top'
      | some bottom' => some (.vsplit top' bottom' ratio)
  | _, _ => some l
def PaneLayout.getAllPaneBounds (l : PaneLayout) (h w : Nat) : List (Nat × Nat × Nat × Nat × Nat) :=
  let rec traverse (node : PaneLayout) (r c h w : Nat) (acc : List (Nat × Nat × Nat × Nat × Nat)) :=
    match node with
    | .pane id _ => (id, r, c, h, w) :: acc
    | .group _ body => traverse body 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 []
private def clampSize (value fallback minValue maxValue : Nat) : Nat :=
  max minValue (min maxValue (if value == 0 then fallback else value))
private def resolveAxisSize (available fallback minValue maxValue : Nat) : FloatingAxisSize → Nat
  | .auto => clampSize fallback fallback minValue maxValue
  | .fixed value => clampSize value fallback minValue maxValue
  | .ratio ratio =>
      let value := (Float.ofNat available * ratio).toUInt64.toNat
      clampSize value fallback minValue maxValue
private def defaultFloatingSizeSpec : FloatingSizeSpec :=
  {
    width := .ratio 0.6
    height := .ratio 0.6
    minWidth := some 24
    minHeight := some 8
  }
private def multiPaneFloatingSizeSpec : FloatingSizeSpec :=
  {
    width := .ratio 0.8
    height := .ratio 0.7
    minWidth := some 60
    minHeight := some 16
  }
private def sizeSpecForPolicy : FloatingSizePolicy → FloatingSizeSpec
  | .default => defaultFloatingSizeSpec
  | .multiPane => multiPaneFloatingSizeSpec
  | .custom spec => spec
def computeFloatingClusterBounds (rows cols idx : Nat) (cluster : FloatingCluster) : Option (Nat × Nat × Nat × Nat) :=
  let availableRows := if rows > 1 then rows - 1 else rows
  if availableRows < 6 || cols < 16 then
    none
  else
    let spec := sizeSpecForPolicy cluster.sizePolicy
    let hMax := availableRows - 2
    let wMax := cols - 4
    let defaultH := max 8 ((availableRows * 3) / 5)
    let defaultW := max 24 ((cols * 3) / 5)
    let minH := spec.minHeight.getD 1
    let minW := spec.minWidth.getD 1
    let maxH := spec.maxHeight.map (min hMax) |>.getD hMax
    let maxW := spec.maxWidth.map (min wMax) |>.getD wMax
    let h := resolveAxisSize availableRows defaultH minH maxH spec.height
    let w := resolveAxisSize cols defaultW minW maxW spec.width
    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 FloatingPaneState.getClusters (layout : PaneLayout) (floating : FloatingPaneState) : Array FloatingCluster :=
  floating.clusters.foldl (fun acc cluster =>
    if layout.containsFloatingRoot cluster.root then acc.push cluster else acc) #[]
def FloatingPaneState.clusterForPane? (layout : PaneLayout) (floating : FloatingPaneState) (paneId : Nat) : Option FloatingCluster :=
  let clusters := floating.getClusters layout
  let rec loop (i : Nat) : Option FloatingCluster :=
    if i >= clusters.size then
      none
    else
      let cluster := clusters[i]!
      match layout.extractFloatingRoot cluster.root with
      | some subtree =>
          if subtree.getPaneIds.contains paneId then some cluster else loop (i + 1)
      | none => loop (i + 1)
  loop 0
end Bliku

import Bliku.Style
namespace Bliku
structure ByteDecoration where
  row : Nat
  startByte : Nat
  endByte : Nat
  priority : Nat := 0
  style : String
  deriving Repr, BEq, Inhabited
structure CellDecoration where
  row : Nat
  startCol : Nat
  endCol : Nat
  priority : Nat := 0
  style : String
  deriving Repr, BEq, Inhabited
structure CursorDecoration where
  row : Nat
  col : Nat
  charStyle : String
  spaceStyle : String
  priority : Nat := 1000
  deriving Repr, BEq, Inhabited
end Bliku