Cairn.Runtime.Step
lean/Cairn/Runtime/Step.lean
The interaction runtime: turns host events into the Actions an app's update sees.
step is two halves. route reads the event against the laid tree on screen and produces
the new interaction state and a list of actions, each naming a control of that tree. step
then hands the actions to app.update in order, re-runs view and layout, and repairs focus,
hover and press against the new tree. The semantics are written out in docs/runtime.md.
Imports Cairn.App, Cairn.UI.Hit, Cairn.VList, Cairn.Layout.Core, Cairn.Runtime.World
Structures 5
Config : Type
What the runtime needs besides the app: text metrics and the layout function. Layout is a parameter so the runtime and its theorems don't depend on one implementation.
metrics : TextMetrics
layout : Laid
panelHeight : IntA panel's height for its content at a width: the content's own (hug) height, measured with that width offered (so paragraphs wrap to it).
State (S : Type) : Type
app : S
ui : UI
Window size, hover, pressed control, focus, window focus. view reads this.
clicks : NatClick count of the pointerDown that started the current press.
pointer : Option Point
Last pointer position in the window, none after it leaves. Hover follows it.
scale : NatBacking scale × 100.
laid : Laid
The laid tree on screen: what the person sees and what hit testing reads.
world : World
The clock, timers, pending requests and subscriptions (docs/effects.md).
subCmds : Array SubCmd
Subscription commands of the most recent stepBytes batch; the frame carries them.
surfaces : List Shown
What each of the app's surfaces shows, in the app's order.
seen : List ControlRef
The controls marked Control.appear that had a visible part at the last Event.frame
(appearRefs): an appear move is delivered for those that have one now and aren't here.
Scroller : Type
A scroll box whose offset the runtime owns, as laid.
ref : ControlRef
rect : Rect
The box's rect, and what of it shows (rect ∩ clip).
visible : Rect
horiz : BoolA row scrolls sideways; a column or a stack up and down.
viewport : IntThe box's length along its axis.
content : IntThe content's length along the axis, from the box's start unscrolled to the furthest child's end plus the end padding (just the padding with no children).
offset : IntThe offset the view laid it at (Style.scroll).
LaidList : Type
A virtual list as laid: its ref, what the view laid it by, its rect and padding, the offset it was laid at, how far that offset can go, and its children.
ref : ControlRef
info : VList.Info
rect : Rect
pad : Insets
offset : Intlimit : Intkids : List Laid
Ctx (S : Type) : Type
An event's progress through the app: its state, the world, the effects that go on the frame, and whether anything was delivered.
Inductive types 1
Shown : Type
What one surface shows now (docs/surfaces.md). The window's content is the state's ui and
laid; a panel's is laid out here at its width and its own height; a status item's is its
description, which menuSelect is checked against.
window (place : ClaimId) (title : String) (minSize : Size) : Shown
The window: its place, title and the smallest content size the app asks for
(App.minSize).
panel (place : ClaimId) (shown : Option (PanelView × Size × Laid)) : Shown
A shown panel: its view, its size (its width, its content's height) and its layout.
status (place : ClaimId) (item : Option StatusItem) : Shown
bar (place : ClaimId) (items : List MenuItem) : Shown
The app's items in the menu bar (Surface.menuBar), which menuSelect is checked
against.
Definitions 101
place : Shown → ClaimId
windowPlace : List Shown → Option ClaimId
The first window's place: where bare local events go.
statusOf (p : ClaimId) : List Shown → Option StatusItem
What status item p shows, if it is shown.
fieldInfo (t : Target) : Option (TextStyle × FieldView × Point)
A field's font, view and text origin.
nearest (offs : List Int) (x : Int) : Nat
The index of the offset nearest x; the earlier one on a tie.
go (x : Int) : List Int → Nat → Option (Nat × Nat) → Option Nat
caretAt (m : TextMetrics) (t : Target) (p : Point) : Nat
The caret boundary a click at p lands on: the nearest entry of the field's caret offsets,
measured from its textOrigin.
fieldLength (t : Target) : Nat
editOps (k : Key) (mods : Mods) : List TextOp
Editing keys on a focused field. Single-line fields: up and page up go home, down and page down go to the end.
replaceOps (t : Target) : Option (Nat × Nat) → List TextOp
Select [a, b) (clamped to the text) before an insert or composition that replaces it.
limit (sc : Scroller) : Int
The furthest an offset can go: max 0 (content − viewport).
mainStart (h : Bool) (q : Rect) : Int
mainLen (h : Bool) (q : Rect) : Int
contentLen (h : Bool) (r : Rect) (pad : Insets) (o : Int) (kids : List Laid) : Int
The content's length of a box laid at r and scrolled by o (Scroller.content): its
children's rects are moved back by o, so their ends unscrolled are their ends plus o.
scrollerOf : Laid → Option Scroller
The scroller a laid node is, if it is a scroll box with a scrollRef.
scrollersOf : Laid → List Scroller
Every scroller in the tree, in paint order (an outer box before the boxes inside it).
scrollersList : List Laid → List Scroller
around (r : ControlRef) : Laid → Option (List Scroller)
The scrollers around the first control r in paint order, outermost first; none when
r isn't in the tree.
aroundList (r : ControlRef) : List Laid → Option (List Scroller)
scrollerAt (laid : Laid) (p : Point) : Option Scroller
The topmost scroller whose visible part holds p: the innermost one there.
clampOff (o lim : Int) : Int
clampScroll (scs : List Scroller) (offs : List (ControlRef × Int)) : List (ControlRef × Int)
The offsets of offs whose box is in the tree, each clamped to its box; the rest dropped.
setScroll (ui : UI) (r : ControlRef) (o : Int) : UI
Set box r's offset to o; the same UI when it already is o.
scrollTo (ui : UI) (sc : Runtime.Scroller) (o : Int) : UI
Move sc to o, clamped.
lineStep : IntHow far an arrow key scrolls, in points.
page (sc : Scroller) : Int
How far a page key scrolls: the viewport less a line, so a line stays in view.
keyScroll (sc : Scroller) (cur : Int) (k : Key) (mods : Mods) : Option Int
Where a key moves sc from cur, if it is a scroll key for it: page up and down, space and
shift-space by a page; home and end to the ends; the arrows along its axis by a line (with
command, to the ends).
revealOff (sc : Scroller) (cur : Int) (q : Rect) : Int
The offset that brings q (a rect laid with sc at cur) into sc's view: the least
move that puts its start and end inside the box, its start when it is longer than the box.
revealIn (chain : List Scroller) (ui : UI) (q : Rect) : UI
Bring q into view in each of chain (outermost first), innermost first: each box moves
it, then the next box out sees it moved.
appearRefs (laid : Laid) : List ControlRef
The controls marked Control.appear with a visible part, in paint order.
appearing (laid : Laid) (seen : List ControlRef) : List Action
The appear moves of a frame: one for each control in appearRefs laid not in seen.
openMenu {S : Type} (s : State S) : Option (ControlRef × ControlMenu)The control menu open now: UI.menu's control and its menu, in the tree on screen.
selectMenu {S : Type} (s : State S) (p : ClaimId) : Option (List MenuItem)The menu a menuSelect p _ is checked against: with the window's place, the control menu
open now (openMenu); otherwise status item p's menu or the menu bar p's items.
openAt {S : Type} (s : State S) (r : ControlRef) : State SOpen control r's menu.
focused {S : Type} (s : State S) : Option TargetThe focused control, looked up in the tree on screen.
leave {S : Type} (s : State S) (next : Option ControlRef) : List ActionLeaving a focused field for next blurs it.
onField {S : Type} (s : State S) (ops : Target → List TextOp) : List ActionEdits to the focused field, if a field is focused.
keyActions {S : Type} (s : State S) (k : Key) (mods : Mods) : List Action
textActions {S : Type} (s : State S) (str : String)
(rep : Option (Nat × Nat)) : List Action
tabOrder (laid : Laid) : List Target
Focusable controls in paint order.
tabTarget {S : Type} (s : State S) (back : Bool) : Option TargetThe next focusable control after the focused one (or before it, going back), wrapping; the first (or last) when nothing is focused.
tab {S : Type} (s : State S) (back : Bool) : State S × List ActionTab and shift-Tab: focus the next (or previous) focusable control, scrolling every scroll box around it so that it is in view.
wheel {S : Type} (s : State S) (p : Point) (dx dy : Int) : State SA wheel or trackpad scroll at p: moves the innermost scroll box there along its axis
(dx in a row, dy otherwise; positive toward the end, trusted ^1012), clamped.
keyScroller {S : Type} (s : State S) : Option ScrollerThe scroll box the keys move: the innermost one around the focused control, else the one under the pointer.
keyScrollState {S : Type} (s : State S) (k : Key) (mods : Mods) : State SA key that no control takes (nothing focused, or a focused control that isn't a field and
doesn't press on it) scrolls keyScroller, if it is a scroll key for it.
withPointer {S : Type} (s : State S) (p : Point) : State S
keyMenu {S : Type} (s : State S) (k : Key) : Option ControlRefThe control whose menu a key opens: the focused control, if it has a menu and the key is the context-menu key, or it is a menu button and the key is Return or Space.
secondaryDown {S : Type} (s : State S) (p : Point) : State SA secondary click at p: hover follows it, and the menu of the control there that has one
(menuTarget) opens; nothing else.
keyRoute {S : Type} (s : State S) (k : Key) (mods : Mods) :
State S × List ActionA key other than Tab: it opens the focused control's menu (keyMenu), or scrolls and acts
as keyScrollState and keyActions say.
textRoute {S : Type} (s : State S) (str : String) (rep : Option (Nat × Nat)) :
State S × List ActionCommitted text: a space on a focused menu button opens its menu (as the Space key does);
anything else is textActions.
route {S : Type} (m : TextMetrics) (s : State S) :
Event → State S × List ActionRead one event against the tree on screen. Returns the new interaction state (app and
laid untouched) and the actions to deliver, in order.
same (a b : UI) : Bool
Structural equality on UI, decided field by field (the derived BEq isn't lawful).
listsOf : Laid → List LaidList
Every virtual list in the tree, in paint order.
listsList : List Laid → List LaidList
recordLists (laid : Laid) : List (ControlRef × VList.Known × Int)
The runtime's record of every virtual list in laid: what is now known of it, and its
corrected offset.
setOff (offs : List (ControlRef × Int)) (r : ControlRef) (o : Int) : List (ControlRef × Int)
offs with box r at o; the same list when it already is (as UI.setScroll).
relayout {S : Type} (app : App S) (cfg : Config) (st : S) (ui : UI) : Laid
onScreen (scs : List Scroller) (r : ControlRef) : Bool
Whether r is a scroll box of scs.
keepOff {α : Type} (on : ControlRef → Bool) (keep : List ControlRef)
(now old : List (ControlRef × α)) : List (ControlRef × α)The entries of xs for boxes kept and not on screen, the ones in now first: what a box
the app keeps (App.keepScroll) had when it left (docs/runtime.md, "Scrolling").
revive (scs : List Scroller) (ui : UI) : List (ControlRef × Int)
The kept offsets of boxes back on screen with no offset of their own: they resume where they were.
fixUI (laid : Laid) (pointer : Option Point) (ui : UI) (keep : List ControlRef) : UI
Repair interaction state against a new tree: hover is what the pointer is over, focus
and press survive only if their control does, and scroll offsets only if their box does, clamped
to its content, or the app keeps it (keep, from App.keepScroll), when it is kept as it was.
A kept box that is back resumes its kept offset. Virtual lists are recorded (recordLists) and
their offsets corrected before the clamp.
settle {S : Type} (app : App S) (cfg : Config) (st : S)
(pointer : Option Point) (ui0 : UI) : Nat → UI → UI × LaidView and lay out, repair ui0 against the result, and repeat while the repair changes
what the view saw (hover reveals, focus rings), up to fuel more times. The result is always
ui0 repaired against the tree returned with it.
settleFuel : NatHow many times settle may re-run the view after the first layout.
unsettled (laid : Laid) : Bool
Whether a virtual list in laid laid a row at a height other than the one the view laid it
out by: a row the runtime hadn't recorded yet, or had recorded at another height. A frame like
that shows heights the list no longer has, and the next layout lays it differently.
rowFuel (laid : Laid) : Nat
How many more layouts resettle may take after settle: the rows of the virtual lists in
laid. A list learns heights one window at a time, so when many rows it knows change at once
(a filter hiding many rows), each layout brings the next window of them in at their old
heights; the rows in the list bound how many windows there are, where a fixed fuel doesn't.
resettle {S : Type} (app : App S) (cfg : Config) (st : S)
(pointer : Option Point) (ui0 : UI) : Nat → UI × Laid → UI × Laid
settleAll {S : Type} (app : App S) (cfg : Config) (st : S)
(pointer : Option Point) (ui0 ui : UI) : UI × Laid
requestedScrolls (effs : List Effect) : List (ControlRef × ScrollTarget)
The scroll requests in effs, in order.
aimOff (laid : Laid) (ui : UI) (r : ControlRef) (to : ScrollTarget) : Option Int
The offset to asks of the box r in the tree laid, clamped as every offset is: start
is 0, finish the box's limit, and key k the top of the row with key k in the heights the
runtime now knows (ui.listOf, which the next layout lays the list by). none when r is no
scroll box on screen, or to is a key and r no virtual list with that key.
aimScroll (goals : List (ControlRef × ScrollTarget)) (laid : Laid) (ui : UI) : UI
Set each requested box's offset, in order (the last request for a box wins).
aim {S : Type} (app : App S) (cfg : Config) (st : S) (pointer : Option Point)
(ui1 : UI) (goals : List (ControlRef × ScrollTarget)) : Nat → UI × Laid → UI × LaidAim the requested boxes against the tree just laid and settle again, while that moves an
offset, up to fuel times: a virtual list laid at a new offset learns the heights of the rows
there, which can move its end or a row's top, so the next round aims at the corrected place.
Each round repairs ui1 (the routed UI) with the aimed offsets and what the last round
recorded, so focus, press and hover are repaired as settle repairs them.
aimFuel : NatHow many rounds aim may take.
lay {S : Type} (app : App S) (cfg : Config) (st : S) (pointer : Option Point)
(goals : List (ControlRef × ScrollTarget)) (ui1 : UI) : UI × LaidSettle ui1 against the app's view, then run the scroll requests goals (aim).
panelSize (cfg : Config) (v : PanelView) : Size
A shown panel's size: its width and its content's height at that width.
layPanel (cfg : Config) (v : PanelView) : Size × Laid
Lay out a shown panel at its size.
show {S : Type} (cfg : Config) (st : S) (min : Size) :
Surface S → ShownWhat one surface shows in app state st; a window keeps the app's smallest size min.
shows {S : Type} (app : App S) (cfg : Config) (st : S) : List ShownWhat every surface shows in app state st.
deliver {S : Type} (update : S → Action → S × List Effect) (st : S)
(acts : List Action) : S × List EffectRun update over the actions in order, collecting effects.
requestedFocus (effs : List Effect) : Option ControlRef
The focus the effects ask for: the last Effect.focus, if any.
applyFocus (effs : List Effect) (ui : UI) : UI
give {S : Type} (app : App S) (c : Ctx S) (m : Msg) : Ctx SDeliver a message to receive and take in its effects.
hear {S : Type} (app : App S) (c : Ctx S) : Ctx STell the app the time, if it hasn't heard the current one.
fire {S : Type} (app : App S) (c : Ctx S) (n : String) : Ctx SFire n if it is still set and due: it leaves the table, then is delivered.
boot {S : Type} (app : App S) (c : Ctx S) : Ctx SOn the first clock: the app hears the time, then initEffects run.
release {S : Type} (c : Ctx S) (w : World) : Ctx SA slot or an id has freed (w is the world after a reply was taken): send what the queue
can, oldest first, onto the frame.
ack {S : Type} (c : Ctx S) (id : Nat) : Ctx SThe host's reply to a request cancelled after it was sent: no one hears it; it frees the slot and the id.
admit {S : Type} (app : App S) (s : State S) : Event → Ctx SWhat the world events deliver: a clock event fires due timers, a reply is delivered if its
id is pending and it answers that kind, and a subscription event if its id is active. Other
events deliver nothing here (their actions come from route). A reply that frees a slot sends
what was queued before the app hears it (docs/effects.md, "Requests in flight").
act {S : Type} (app : App S) (c : Ctx S) (acts : List Action) : Ctx SDeliver the routed actions to update (after the time, if the app hasn't heard it) and take
in their effects, in order.
step {S : Type} (app : App S) (cfg : Config) (s : State S) (e : Event) :
State S × List EffectOne event.
frameEvents : List Event
What steps runs after a batch's events: two frame events, so that what an appear move's
own delivery brings into view is heard in the same batch (docs/runtime.md, "Appear").
letGo (ui : UI) : UI
What the runtime knows once a frame is shown: every virtual list's held anchor let go
(VList.Known.letGo), so each list keeps its rows where this frame shows them. Within a batch
the reader sees none of the frames between, so an anchor the clamp moved is held at the place
the reader last saw it until then (VList.anchorAt).
shown {S : Type} (s : State S) : State SA state whose frame has been shown (UI.letGo).
steps {S : Type} (app : App S) (cfg : Config) (s : State S)
(es : List Event) : State S × List EffectA batch of events, in order, then frameEvents; then the frame is shown (State.shown).
start {S : Type} (app : App S) (cfg : Config) (size : Size)
(scale : Nat := 100) : State SThe first state: the app's init at a window size, laid out, with the app's initFocus
if that control is focusable.
cursor {S : Type} (s : State S) : CursorThe cursor the host shows: text over fields, a pointing hand over other controls.
Theorems 1
same_eq {a b : UI} (h : same a b = true) : a = b
Instances 2
instInhabitedShown : Inhabited Shown
instInhabitedScroller : Inhabited Scroller
Fields
Scrolling (docs/runtime.md, "Scrolling")
The runtime owns the offset of every scroll box with a Style.scrollRef, as it owns focus: it
keeps them in UI.scroll, the wheel, the trackpad and the scroll keys move them, Tab into a box
brings the focus into view, and fixUI clamps them to the box's content after every layout. The
view only reads them (UI.scrollOf, UI.scrolling); a scroll never reaches update.
Appear
Menus on controls (docs/surfaces.md, "Menus on controls")
Routing
Committing
Virtual lists (docs/runtime.md, "Virtual lists")
After every layout the runtime records what it learnt of each virtual list on screen
(VList.record): the heights of the rows just laid, the box's length, and the row to keep still,
and it moves the list's offset by as much as that row's top moved. The view reads the record
back (VList.node, through UI.listOf), so the next layout lays those rows at their real
heights.