Cairn.Runtime.World
lean/Cairn/Runtime/World.lean
The runtime's view of the outside world (docs/effects.md): the clock, the app's timers, its
pending requests and its active subscriptions. Pure tables and the functions that update them;
Cairn.Runtime.Step decides when they run, and Cairn.Runtime.WorldProofs says what they
guarantee.
Imports Cairn.Input
Structures 1
World : Type
booted : BoolWhether the first clock event has arrived (and App.initEffects run).
timers : List (String × Nat)
Timers: name and due time (monotonic ms), in the order they were set.
pending : List (Nat × Request.Kind)
Requests sent and not yet answered or cancelled: id and kind. Only these replies reach the app.
queued : List (Nat × Nat × Request)
Requests not yet sent, oldest first: a ticket (from nextTicket), the id and the request.
Each waits for a slot (cap) or for its id's cancelled request to be answered.
stopping : List (Nat × Request.Kind)
Requests cancelled after they were sent: id and kind. Each keeps its slot and its id until
the host's one reply to it, which no one hears (takeStop).
cap : NatThe most requests of capped kinds (Request.Kind.capped) with the host at once:
App.maxInFlight.
nextTicket : NatThe ticket the next queued request gets.
subs : List (Nat × Sub)
Active subscriptions under the ids the host knows them by.
nextSub : NatThe id the next new subscription gets.
Definitions 27
tick (w : World) (t : Time) : World
A new time from the host. The monotonic part never goes back.
timerNames (w : World) : List String
setTimer (w : World) (n : String) (ms : Nat) : World
(Re)start n, due ms from now; it goes to the end of the order.
cancelTimer (w : World) (n : String) : World
dueNow (w : World) (n : String) : Bool
n is set and due at the current time.
dueNames (w : World) : List String
The timers due now, earliest first; ties in the order they were set (mergeSort is
stable).
wake (w : World) : Option Nat
The earliest deadline, if any timer is set: the frame's wake.
waiting (w : World) : List (Nat × Request)
The queued requests, without their tickets.
entries (w : World) : List (Nat × Request.Kind)
The requests the app may still hear about, sent or not: id and kind.
live (w : World) (id : Nat) : Option Request.Kind
What the app may still hear about id: its kind if it is pending or queued.
isLive (w : World) (id : Nat) : Bool
id is pending or queued: a request under it is refused.
isStopping (w : World) (id : Nat) : Bool
id was cancelled after it was sent and the host has not answered it yet.
inFlight (w : World) : Nat
Requests of capped kinds with the host: pending or stopping.
canSend (w : World) (id : Nat) (k : Request.Kind) : Bool
A request can go to the host now: its id is not still stopping, and a capped one has a slot.
send (w : World) (id : Nat) (k : Request.Kind) : World
enqueue (w : World) (id : Nat) (r : Request) : World
cancel (w : World) (id : Nat) : World × Bool
Withdraw id: a queued request leaves the queue and was never sent (nothing on the frame);
a pending one moves to stopping and its cancel goes on the frame for the host.
absorb1 (w : World) : Effect → World × Bool
Take in one effect of a delivery. Returns whether it goes on the frame now: a request whose
id is pending or queued is refused (never sent, never answered); a request that can't be sent
yet is queued (it goes on a later frame, from promote); a cancel goes only for a request that
was sent; everything else goes.
absorb (w : World) : List Effect → World × List Effect
Take in a delivery's effects, in order; returns the ones that go on the frame.
takeReply (w : World) (id : Nat) (r : Reply) : Option World
A reply to id: when id is pending and r answers its kind, the world without it.
takeStop (w : World) (id : Nat) : Option World
The host's reply to a request cancelled after it was sent: it is forgotten, and its slot and id are free again.
promoteGo (w : World) : List (Nat × Nat × Request) → World × List Effect
Go through queued requests in order, sending each that can be sent at its turn and keeping
the rest (in order) in w.queued.
promote (w : World) : World × List Effect
After a slot or an id frees: send every queued request that can go now, oldest first. Returns the requests for the frame.
subOf (w : World) (id : Nat) : Option Sub
The active subscription with this id.
number : Nat → List Sub → List (Nat × Sub)
Number subscriptions from next.
freshSubs (seen : List Sub) : List Sub → List Sub
The subscriptions in want that are not among seen, without repeats, in order.
diffSubs (active : List (Nat × Sub)) (want : List Sub) (next : Nat) : List (Nat × Sub) × List SubCmd × Nat
Diff the active subscriptions against what the app asks for now. Returns the new active set, the commands for the host (stops first, then starts), and the next free id.
Instances 2
instReprWorld : Repr World
instInhabitedWorld : Inhabited World