The view and layout · Cairn docs

An app's view is a pure function from its state to a tree of nodes. Lean lays the tree out, hit tests it, and turns it into the frame the host paints. Because all of that is Lean, "the item's delete button is on screen" and "a click at its centre presses it" are theorems about the code that actually runs, not about a model of it.

The view function

A window's view takes the app's state and the UI state: the window's size, which control the pointer is over, which is pressed, which has keyboard focus. The runtime keeps the UI state; the view only reads it, for hover colours and focus rings. The fixture's button:

def button (ui : UI) (r : ControlRef) (label : String) : Node :=
  .box { padding := ⟨6, 16, 6, 16⟩, radius := 6, border := ring ui r,
         background := some (if ui.hover = some r then accentDark else accent) }
    (some { ref := r, label })
    [.text { font := { body with weight := 600 }, color := white } label]

test/fixture/lean/Fixture.lean, lines 631–635

A node that performs a move carries a control: the ref of the claim it performs, an accessibility role and a label. Controls are how presence theorems, hit testing and the accessibility mirror find a move on screen. The host gives each control's accessibility element the identifier ^N.

inductive Role where
  | group | button | checkbox | text | textField | link | list | listItem | heading | tab
  /-- A scroll box (`Style.scroll`): the frame gives one a node of its own. -/
  | scrollArea
deriving Repr, BEq, DecidableEq, Inhabited

/-- A node that performs a move. -/
structure Control where
  ref : ControlRef
  role : Role := .button
  label : String
  value : String := ""
  checked : Option Bool := none
  selected : Bool := false
  /-- Tell the app when this control comes on screen: the runtime delivers `Action.appear` when
  it has a visible part at the end of a batch and didn't at the end of the last one (or wasn't
  in the tree). How an app hears that the end of a list is in view (docs/runtime.md, "Appear"). -/
  appear : Bool := false
deriving Repr, BEq, Inhabited

lean/Cairn/UI/Node.lean, lines 164–182

Nodes

There are four kinds of node: a box, a line of text, wrapped text, and a text field.

inductive Node where
  | box (style : Style) (control : Option Control) (children : List Node)
  | text (style : TextStyle) (content : String)
  /-- Text wrapped at word boundaries to the available width (`Cairn.Text.Wrap`). Layout turns
  it into a clipping column of one `text` per line, so it has no `Laid` form of its own. -/
  | para (style : TextStyle) (wrap : Wrap) (content : String)
  | field (style : Style) (text : TextStyle) (control : Control) (view : FieldView)
deriving Repr, Inhabited

lean/Cairn/UI/Node.lean, lines 316–323

A box has a style: how it lays out its children, how big it is, and how it is painted.

structure Style where
  axis : Axis := .column
  width : Sizing := .hug
  height : Sizing := .hug
  padding : Insets := {}
  gap : Nat := 0
  /-- Cross-axis alignment of children. -/
  align : Align := .start
  /-- Main-axis placement of children when there's space left over. -/
  justify : Align := .start
  background : Option Color := none
  border : Option Border := none
  radius : Nat := 0
  /-- Clip children to this box. -/
  clip : Bool := false
  corner : Corner := .circular
  /-- Painted under the box's background. -/
  shadow : Option Shadow := none
  /-- Host-drawn pixels over the background, under the children. -/
  paint : Option Paint := none
  /-- A loaded image over the background (and the paint), under the children. -/
  image : Option ImageFill := none
  /-- A scroll box: `some o` lays the children out as the box's axis says,
  then moves them back by `o` points along that axis (up, or left in a row), and clips them to
  the box. `none` is an ordinary box. The children keep their real rects, possibly above or
  below the box; what shows is `rect ∩ clip` (docs/layout.md, "Scroll boxes"). -/
  scroll : Option Int := none
  /-- The scroll box's identity, when the runtime owns its offset (docs/runtime.md,
  "Scrolling"): the wheel, the trackpad and the page keys move it, and the view reads it back with
  `UI.scrollOf` (`UI.scrolling` sets both fields). Usually a `place` claim's ref. A box with
  `scroll` and no `scrollRef` scrolls only as far as the view says. -/
  scrollRef : Option ControlRef := none
  /-- A virtual list's box (`Cairn.VList`): which rows it laid and the heights it laid them
  by. The runtime records the rows' real heights from it after every layout. Set by `VList.node`
  only. -/
  rows : Option VList.Info := none
  /-- The menu of this box's control (`ControlMenu`); ignored on a box without a control. -/
  menu : Option ControlMenu := none
deriving Repr, BEq, Inhabited

lean/Cairn/UI/Node.lean, lines 227–265

Layout

Layout is a small subset of flexbox, and everything is in integer logical points, origin at the top left, y down. There are no floats anywhere a theorem looks.

/-- `fill` shares the parent's leftover main-axis space equally among `fill` children, and
takes the parent's full cross-axis size. -/
inductive Sizing where
  | fixed (n : Nat) | hug | fill
deriving Repr, BEq, DecidableEq, Inhabited

lean/Cairn/UI/Node.lean, lines 38–42

A row lays its children out left to right, a column top to bottom, and a stack places them all in the same box, later ones on top.
On each axis a node is fixed n, hug (its content's size) or fill. fill children share what is left over equally, to the point: the shares add up exactly, and differ by at most one.
Nothing shrinks. When children don't fit, fill children get nothing and the rest overflow. A box with clip cuts its children to its rect.
There is no scrolling yet.

Text comes from the host's measurements: Lean asks Core Text how wide a string is in a given font, and lays it out with the answer. That the measurement matches what is painted is an assumption, checked by fuzzing; every layout theorem holds for whatever valid measurements the host returns.

Wrapped text and fields

Node.para wraps text to the width it is offered. Lean picks the line breaks from one measurement of the whole string, so the paragraph rewraps as the window resizes, and theorems say every line fits, nothing is lost or reordered, and maxLines is respected. From the fixture's view:

.para { font := { size := 13 }, color := muted } {}
  "Cairn's test app. Type an item and press Enter or Add, check it off or delete it, and \
   press Flash to set a timer. Lean breaks this paragraph to the window's width.",

test/fixture/lean/Fixture.lean, lines 745–747

A field shows a Text.Field: its text, caret, selection and input-method composition. The field's move edits it (chapter 2), and the view shows it:

def inputRow (s : State) (ui : UI) : Node :=
  .box { axis := .row, width := .fill, gap := 8, align := .center } none
    [ .field { width := .fill, padding := ⟨6, 8, 6, 8⟩, background := some white, radius := 6,
               border := ring ui fieldRef (some ⟨1, line⟩) }
        { font := body, color := ink }
        { ref := fieldRef, role := .textField, label := placeholder }
        (s.field.view (ui.focus = some fieldRef)),
      button ui addRef "Add" ]

test/fixture/lean/Fixture.lean, lines 639–646

Lists

A list is a box whose children come from the state: the fixture's view (chapter 1) maps itemRow over its items. Each row's controls use a key, the item's id, so ^4#12 is item 12's checkbox wherever it ends up:

/-- An item's menu: on its ⋯ button and its checkbox (docs/surfaces.md, "Menus on controls"). -/
def itemMenuItems (it : Item) : List MenuItem :=
  [ .item { ref := menuToggleRef it.id, label := if it.done then "Mark Not Done" else "Mark Done" },
    .item { ref := menuDeleteRef it.id, label := "Delete" } (enabled := it.done),
    .separator,
    .info s!"Item {it.id}" ]

def itemRow (ui : UI) (it : Item) : Node :=
  .box { axis := .row, width := .fill, height := .fixed 36, gap := 10, align := .center,
         padding := ⟨0, 8, 0, 10⟩, background := some white, radius := 6 } none
    [ .box { width := .fixed 18, height := .fixed 18, radius := 4, align := .center,
             justify := .center,
             background := some (if it.done then accent else white),
             border := ring ui (toggleRef it.id) (if it.done then none else some ⟨1, line⟩),
             menu := some { items := itemMenuItems it } }
        (some { ref := toggleRef it.id, role := .checkbox, label := it.text,
                checked := some it.done })
        (if it.done then [.text { font := { size := 12, weight := 700 }, color := white } "✓"]
         else []),
      .text { font := body, color := if it.done then muted else ink } it.text,
      .box { width := .fill } none [],
      .box { padding := ⟨3, 8, 3, 8⟩, radius := 4, border := ring ui (deleteRef it.id),
             background := some ⟨240, 240, 242, 255⟩ }
        (some { ref := deleteRef it.id, label := s!"Delete {it.text}" })
        [.text { font := { size := 13 }, color := ⟨200, 40, 40, 255⟩ } "Delete"],
      .box { padding := ⟨3, 8, 3, 8⟩, radius := 4, border := ring ui (moreRef it.id),
             background := some (if ui.menu = some (moreRef it.id) then line else ⟨240, 240, 242, 255⟩),
             menu := some { items := itemMenuItems it, button := true } }
        (some { ref := moreRef it.id, label := s!"More for {it.text}" })
        [.text { font := { size := 13, weight := 700 }, color := ink } "⋯"] ]

test/fixture/lean/Fixture.lean, lines 657–686

Rigid views

A view whose boxes are fixed in size and clip their text is rigid: no rect depends on the width of a string. For a rigid view, Cairn can prove every control is pressable in every state, with any text measurements, in any window above a minimum size; the next chapter says how. A counter with fixed-size buttons is rigid. The fixture isn't: its buttons hug their labels. A view whose layout depends on its text can still be checked, one concrete layout at a time, and the fuzzer checks every control it lays out.

Surfaces

An app shows a fixed list of surfaces: at most one window, overlay panels that never take focus or clicks, and menu bar items with native menus built from Lean. Each is identified by a place claim. The fixture has just its window.

/-- One thing an app shows (docs/surfaces.md). An app declares a fixed list of them; whether
each is shown, and what it shows, is a function of the state. `place` is the surface's place
claim: its durable identity on the wire, in the map and in the debug socket. -/
inductive Surface (S : Type) where
  /-- M1's window: Metal content laid out at the window's size, with input. -/
  | window (place : ClaimId) (title : String) (view : S → UI → Node)
  /-- A non-activating, click-through overlay panel; `none` hides it. It takes no input, so its
  view doesn't read `UI`. The view is given the text metrics the panel is laid out with, so it
  can measure content (`Cairn.Layout.measure`), for instance to animate between two heights. -/
  | panel (place : ClaimId) (view : TextMetrics → S → Option PanelView)
  /-- A menu bar status item and its native menu; `none` removes it from the menu bar. -/
  | statusItem (place : ClaimId) (view : S → Option StatusItem)
  /-- The app's own items in the main menu bar (docs/surfaces.md, "The app's menus"). A top-level
  `submenu` is a menu of its own in the menu bar, after the app menu, in order (Go, View); every
  other top-level entry goes in the app menu, after the app's name and before Hide and Quit,
  which stay the host's. An item's shortcut is its key equivalent, honoured whenever the app is
  active. Shown only while the app has a window: an accessory app has no main menu. -/
  | menuBar (place : ClaimId) (view : S → List MenuItem)

lean/Cairn/App.lean, lines 76–93