Terminus Apps

Terminus TUI Apps

Build terminal user interface applications in Lean 4 using the Terminus library.

Quick Start

import Terminus

structure AppState where
  count : Int := 0
  deriving Repr, Inhabited

def draw (frame : Frame) (state : AppState) : Frame := Id.run do
  let mut buf := frame.buffer.fill Cell.empty
  let msg := s!"Count: {state.count} (arrows to change, q to quit)"
  buf := buf.writeString 2 2 msg (Style.bold.withFg Color.cyan)
  { frame with buffer := buf }

def update (state : AppState) (event : Option Event) : AppState × Bool :=
  match event with
  | some (.key k) =>
    match k.code with
    | .char 'q' => (state, true)
    | .up => ({ state with count := state.count + 1 }, false)
    | .down => ({ state with count := state.count - 1 }, false)
    | _ => (state, false)
  | _ => (state, false)

def main : IO Unit := App.runApp AppState.mk draw update

Architecture (MUV Pattern)

Terminus uses Model-Update-View architecture:

┌─────────────────────────────────────────────────────────┐
│                     Game Loop                            │
│  ┌──────────┐    ┌──────────┐    ┌──────────┐           │
│  │  Events  │───→│  Update  │───→│   Draw   │───→ Screen│
│  │  poll    │    │ State→   │    │ Frame→   │           │
│  └──────────┘    │ State×   │    │ Frame    │           │
│       ↑          │ Bool     │    └──────────┘           │
│       │          └──────────┘          ↓                │
│       └────────────────────────────────┘                │
└─────────────────────────────────────────────────────────┘

Key Functions:

• draw : Frame → State → Frame - Render state to frame buffer
• update : State → Option Event → State × Bool - Handle input, return (newState, shouldQuit)

Core Types

Color Examples

Color.red                    -- ANSI red
Color.cyan                   -- ANSI cyan
Color.rgb 255 128 0          -- True color orange
Color.indexed 240            -- 256-palette color
Color.ansi .brightBlue       -- Bright blue

Style Examples

Style.bold                           -- Bold text
Style.default.withFg Color.red       -- Red foreground
Style.bold.withFg Color.cyan         -- Bold cyan
Style.default.withBg Color.blue.withFg Color.white  -- White on blue

Input Handling

Event Polling

let event ← Events.poll  -- Non-blocking, returns Event.none if no input

match event with
| .none => ...                    -- No input this frame
| .key k => ...                   -- Keyboard event
| .mouse m => ...                 -- Mouse event
| .resize width height => ...     -- Terminal resized

Key Events

Common Key Codes

.char 'a'       -- Letter 'a'
.enter          -- Enter key
.escape         -- Escape key
.space          -- Spacebar
.up, .down, .left, .right  -- Arrow keys
.backspace      -- Backspace
.tab            -- Tab
.f 1            -- F1 (through .f 12)

Common Key Patterns

match k.code with
| .char 'q' => (state, true)               -- Quit
| .char c => handleChar state c            -- Any character
| .up | .char 'k' => moveUp state          -- Up or vim 'k'
| .down | .char 'j' => moveDown state      -- Down or vim 'j'
| _ => (state, false)                      -- Ignore other keys

-- Ctrl+C check
if k.isCtrlC then return (state, true)

Mouse Events

match event with
| .mouse m =>
  if m.isLeftClick then
    handleClick state m.x m.y
  else if m.isScroll then
    handleScroll state m.button
  else
    (state, false)

Terminal Lifecycle

Simple: App.runApp

def main : IO Unit := App.runApp initialState draw update

Handles setup/teardown automatically. Good for most apps.

Custom Loop (for timing context)

def tick (term : Terminal) (state : GameState) : IO (Terminal × GameState × Bool) := do
  let event ← Events.poll
  let (newState, shouldQuit) := update state (some event)
  let frame := Frame.new term.area
  let frame := draw frame newState
  let term := term.setBuffer frame.buffer
  let term ← term.flush frame.commands
  pure (term, newState, shouldQuit)

partial def runLoop (term : Terminal) (state : GameState) : IO Unit := do
  let (term, state, shouldQuit) ← tick term state
  if shouldQuit then return
  IO.sleep 16  -- ~60 FPS
  runLoop term state

def run : IO Unit := do
  let initialState := GameState.new
  Terminal.setup
  try
    let term ← Terminal.new
    runLoop term initialState
  finally
    Terminal.teardown

Rendering

Buffer Operations

-- Clear buffer
buf := buf.fill Cell.empty

-- Write text
buf := buf.writeString x y "Hello" Style.bold

-- Write styled text
buf := buf.writeString x y "Error" (Style.default.withFg Color.red)

-- Set single cell
buf := buf.set x y (Cell.styled '█' (Style.default.withFg Color.blue))

-- Write with bounds checking
buf := buf.writeStringBounded x y maxWidth "Long text..." style

Centering Content

let area := frame.area
let contentWidth := 40
let contentHeight := 10
let startX := (area.width - contentWidth) / 2
let startY := (area.height - contentHeight) / 2

Drawing Borders

def drawBorder (buf : Buffer) (x y w h : Nat) (style : Style) : Buffer := Id.run do
  let mut b := buf
  -- Corners
  b := b.writeString x y "╭" style
  b := b.writeString (x + w - 1) y "╮" style
  b := b.writeString x (y + h - 1) "╰" style
  b := b.writeString (x + w - 1) (y + h - 1) "╯" style
  -- Horizontal lines
  for i in [1 : w - 1] do
    b := b.writeString (x + i) y "─" style
    b := b.writeString (x + i) (y + h - 1) "─" style
  -- Vertical lines
  for i in [1 : h - 1] do
    b := b.writeString x (y + i) "│" style
    b := b.writeString (x + w - 1) (y + i) "│" style
  b

Widgets

Widget Rendering

-- Create widget
let block := Block.rounded
  |>.withTitle "My App"
  |>.withTitleStyle Style.bold
  |>.withBorderStyle (Style.default.withFg Color.cyan)

let para := Paragraph.fromLines ["Line 1", "Line 2"]
  |>.centered
  |>.withStyle Style.bold
  |>.withBlock block

-- Render to frame
let frame := frame.render para contentArea

Layout System

Constraints

Constraint.fixed 10      -- Exactly 10 cells
Constraint.percent 50    -- 50% of available space
Constraint.min 5         -- At least 5 cells
Constraint.max 20        -- At most 20 cells
Constraint.fill          -- Take remaining space

Splitting Areas

-- Vertical split
let sections := vsplit area [.fixed 3, .fill, .fixed 1]
-- sections[0] = header (3 rows)
-- sections[1] = content (remaining)
-- sections[2] = footer (1 row)

-- Horizontal split
let cols := hsplit area [.percent 30, .fill]
-- cols[0] = left sidebar (30%)
-- cols[1] = main content (70%)

Common Patterns

Game State Template

structure GameState where
  board : Array (Array Cell)
  cursor : Nat × Nat
  score : Nat
  gameOver : Bool
  paused : Bool
  rng : StdGen
  deriving Repr, Inhabited

def GameState.new (seed : UInt64) : GameState := {
  board := Array.mkArray 10 (Array.mkArray 10 Cell.empty)
  cursor := (0, 0)
  score := 0
  gameOver := false
  paused := false
  rng := mkStdGen seed.toNat
}

Universal Key Handling

def update (state : GameState) (event : Option Event) : GameState × Bool :=
  match event with
  | none => (state, false)
  | some (.key k) =>
    -- Always allow quit
    if k.code == .char 'q' || k.isCtrlC then
      return (state, true)
    -- Always allow restart
    if k.code == .char 'r' then
      return (GameState.new state.seed, false)
    -- Block input if paused/game over
    if state.paused || state.gameOver then
      return (state, false)
    -- Handle game input
    handleGameInput state k
  | _ => (state, false)

Overlay Dialogs

def renderOverlay (buf : Buffer) (msg : String) (area : Rect) : Buffer := Id.run do
  let w := msg.length + 4
  let h := 5
  let x := (area.width - w) / 2
  let y := (area.height - h) / 2
  let mut b := buf
  -- Semi-transparent background
  for dy in [0 : h] do
    for dx in [0 : w] do
      b := b.set (x + dx) (y + dy) (Cell.styled ' ' (Style.default.withBg Color.black))
  -- Border and message
  b := drawBorder b x y w h Style.bold
  b := b.writeString (x + 2) (y + 2) msg Style.bold
  b

Animation Timing

structure AnimState where
  timer : Nat := 0
  phase : Nat := 0

def tickAnim (anim : AnimState) : AnimState :=
  if anim.timer > 0 then
    { anim with timer := anim.timer - 1 }
  else
    { anim with phase := (anim.phase + 1) % 4, timer := 5 }

Complete Templates

Game App

import Terminus

namespace MyGame

structure GameState where
  score : Nat := 0
  gameOver : Bool := false
  deriving Repr, Inhabited

def draw (frame : Frame) (state : GameState) : Frame := Id.run do
  let mut buf := frame.buffer.fill Cell.empty
  buf := buf.writeString 2 1 s!"Score: {state.score}" Style.bold
  if state.gameOver then
    buf := buf.writeString 2 3 "GAME OVER - Press R to restart"
      (Style.bold.withFg Color.red)
  { frame with buffer := buf }

def update (state : GameState) (event : Option Event) : GameState × Bool :=
  match event with
  | some (.key k) =>
    match k.code with
    | .char 'q' => (state, true)
    | .char 'r' => (GameState.mk, false)
    | .space => ({ state with score := state.score + 1 }, false)
    | _ => (state, false)
  | _ => (state, false)

end MyGame

def main : IO Unit := App.runApp MyGame.GameState.mk MyGame.draw MyGame.update

CLI + TUI Hybrid

import Terminus
import Parlance

namespace MyTool

-- CLI mode (default)
def runCli (args : List String) : IO Unit := do
  IO.println "CLI mode - use 'mytool tui' for interactive"

-- TUI mode
def runTui : IO Unit := do
  App.runApp initialState draw update

def main (args : List String) : IO Unit := do
  if args.contains "tui" then
    runTui
  else
    runCli args

end MyTool

Projects Using Terminus

Reference implementations in this workspace:

• apps/blockfall - Tetris clone with animations
• apps/minefield - Minesweeper with flood-fill
• apps/solitaire - Card game with undo
• apps/tracker - Issue tracker CLI with TUI mode
• apps/lighthouse - File browser
• apps/enchiridion - Documentation viewer

lakefile.lean Setup

require terminus from git "https://github.com/nathanial/terminus" @ "v0.0.1"

@[default_target]
lean_lib MyApp

lean_exe myapp where
  root := `Main