Cairn.Runtime.Abi
lean/Cairn/Runtime/Abi.lean
The Lean side of the app ABI. The host (workstream G) loads one app per binary and calls
three exported functions; each app file defines them by applying these generic functions to
its App, a Config and a Boundary:
@[export cairn_app_init]
def appInit (w h scalePercent : UInt32) : Runtime.State MyApp.State :=
Runtime.initState MyApp.app cfg w h scalePercent
@[export cairn_app_step]
def appStep (s : Runtime.State MyApp.State) (events : ByteArray) : Runtime.State MyApp.State :=
Runtime.stepBytes MyApp.app cfg boundary s events
@[export cairn_app_frame]
def appFrame (s : Runtime.State MyApp.State) : ByteArray := Runtime.frameBytes boundary s
Lean 4.35 rejects @& on @[export], so every argument is owned: the host passes its
reference to the state into cairn_app_step and keeps the one that comes back, and calls
lean_inc on the state before cairn_app_frame if it keeps using it. See docs/runtime.md.
Imports Cairn.Runtime.Step, Cairn.Frame, Cairn.Frame.Menu
Structures 1
Boundary : Type
The byte formats at the boundary: Cairn.Frame.boundary (Frame.ofLaid and the v1
encoding, docs/frame.md).
decode : List Event
Host event bytes → events, in order.
render : Canvas
The draws, accessibility nodes and text input of a laid tree. It reads the UI for the
surface's size and focus (the caret, AxNode.focused, textInput). The runtime fills in the
cursor, the other surfaces and the effects.
encode : ByteArrayDefinitions 6
initState {S : Type} (app : App S) (cfg : Config)
(w h scalePercent : UInt32) : State S
stepBytes {S : Type} (app : App S) (cfg : Config) (b : Boundary) (s : State S)
(events : ByteArray) : State SRun a batch of events. The state's effects become this batch's effects.
panelUI (size : Size) : UI
A panel's UI: its size, and nothing focused, hovered or pressed (it takes no input).
surfaceFrame {S : Type} (b : Boundary) (s : State S) : Shown → SurfaceFrameOne surface's record. The window shows the state's laid tree; a panel its own.
frame {S : Type} (b : Boundary) (s : State S) : Frame
frameBytes {S : Type} (b : Boundary) (s : State S) : ByteArray