Effects and the host

/-- Runtime → app, through `App.receive`: the outside world. -/
inductive Msg where
  /-- The current time, delivered before anything else whenever it changed. -/
  | clock (t : Time)
  /-- A timer the app set has come due. -/
  | timer (name : String)
  /-- The answer to request `id`. -/
  | reply (id : Nat) (r : Reply)
  /-- An event from an active subscription. -/
  | sub (s : Sub) (e : SubEvent)
deriving Repr, BEq, Inhabited

/-- App → host (and runtime). -/
inductive Effect where
  | setClipboard (s : String)
  | beep
  /-- Move keyboard focus to the control `c`. The runtime runs this one, not the host: after the
  step's actions it sets `ui.focus := some c`, and keeps it only if `c` is a focusable control
  of the new tree (docs/runtime.md). No `blur` is delivered for a field it takes focus from.
  The host decodes it and does nothing. -/
  | focus (c : ControlRef)
  /-- Start (or restart) the timer `name`, due `ms` milliseconds from now. The runtime keeps
  timers; the host only wakes it (docs/effects.md). -/
  | setTimer (name : String) (ms : Nat)
  /-- Forget the timer `name`; nothing if it isn't set. -/
  | cancelTimer (name : String)
  /-- Ask the host to do `r`; it answers with `Msg.reply id _`, exactly once. At most
  `App.maxInFlight` requests of capped kinds (`Request.Kind.capped`) are with the host at a time;
  the runtime holds the rest and sends them, oldest first, as slots free. -/
  | request (id : Nat) (r : Request)
  /-- Withdraw request `id` (docs/effects.md, "Requests in flight"). Its reply never reaches the
  app. A request still waiting for a slot is dropped and never sent; one already sent is cancelled
  on the host (`URLSessionTask.cancel`), and its id stays taken until the host's one reply to it
  arrives, which the runtime swallows. Nothing if `id` is not pending. -/
  | cancelRequest (id : Nat)
  /-- End the app. The host terminates after running the frame's other effects. -/
  | quit
  /-- Move the scroll box or virtual list `box` (its `Style.scrollRef`) to `to`, clamped as every
  offset is. The runtime runs this one, like `focus`: after the step's deliveries and layout it
  sets the offset against the tree just laid and lays out again (docs/runtime.md, "Scrolling").
  A box not on screen is left alone. The host decodes it and does nothing. -/
  | scrollTo (box : ControlRef) (to : ScrollTarget)
  /-- Set the Dock tile's badge to `label`; `none` clears it (docs/effects.md, "The Dock badge
  and announcements"). The host shows exactly the label; Lean decides what it says. -/
  | badge (label : Option String)
  /-- Ask assistive apps (VoiceOver) to speak `text`, for news that has no focus of its own
  ("Couldn't like the post; it's back as it was"). Posted once, with exactly this text. -/
  | announce (text : String) (priority : Priority)
deriving Repr, BEq, Inhabited

/-- The timer Flash sets, and how long the note shows. -/
def flashTimer : String := "flash"
def flashMs : Nat := 400

move ^6 flashMove (s : State) "Flash" in ^1 where
  does "Press Flash."
  sees "A note shows, and goes when the timer the press set fires."
  on press
    emit := ({ s with flash := true }, [.setTimer flashTimer flashMs])
    post s' := s'.flash = true ∧ s'.items = s.items
    sound := by intro s; exact ⟨rfl, rfl⟩

/-- Whether a message is Flash's timer. -/
def isFlash : Msg → Bool
  | .timer n => n == flashTimer
  | _ => false

/-- The world's messages: Flash's timer clears the note; replies and timers of the likes go to
`Like.receive`. -/
def receive (s : State) (m : Msg) : State × List Effect :=
  let o := Like.receive false s.likes s.nextReq m
  ({ s with flash := if isFlash m then false else s.flash, likes := o.1, nextReq := o.2.1 }, o.2.2)

/-- Something the host does that answers back. Closed: adding a kind is a constructor, its
encoding, a `Reply.answers` case and one host handler (docs/effects.md). -/
inductive Request where
  | readFile (path : String)
  /-- Replace the file atomically, creating missing parent directories. -/
  | writeFile (path : String) (data : ByteArray)
  /-- A named system sound ("Tink", "Pop", "Basso", …). -/
  | playSound (name : String)
  /-- An HTTP request. With a `secret`, the host adds its header as it sends (a missing secret
  answers `failed notFound` and sends nothing). With a non-empty `capture`, a 2xx reply whose
  body is a JSON object has each listed top-level string field (`(field, account)`) written to
  the Keychain item `account` and its value replaced by `""` in the body Lean receives; all or
  nothing: a body that isn't a JSON object, or a listed field that is missing, repeated or not
  a string, answers `failed invalid` and writes nothing. Other replies pass through as they
  came. With `redact`, the request carries a secret the person typed (a secure field's text,
  `Cairn.Text.SecureField`): every dump, log and report prints its URL, headers and body as
  `<redacted N bytes>`, and the host sends it as given. -/
  | http (method url : String) (headers : List (String × String)) (body : ByteArray)
      (timeoutMs : Nat) (secret : Option Secret := none)
      (capture : List (String × String) := []) (redact : Bool := false)
  /-- Append to the file, creating it (mode 600) and missing parent directories. -/
  | appendFile (path : String) (data : ByteArray)
  /-- The names in a directory (not `.` and `..`), sorted by their UTF-8 bytes. -/
  | listDir (path : String)
  /-- Remove a file or a symbolic link; never a directory. -/
  | deleteFile (path : String)
  /-- The app in front: its process id and name. -/
  | frontmostApp
  /-- Whether the app holds `p`; with `prompt`, the system also asks the person if it doesn't. -/
  | permission (p : Permission) (prompt : Bool)
  /-- Bring process `pid` to the front and type `text` into it as key events, then Return if
  `pressReturn`. Needs Accessibility. -/
  | typeText (pid : Nat) (text : String) (pressReturn : Bool)
  /-- `http` with a body of parts the host assembles and an optional secret header (OpenAI's
  transcription request: multipart framing from Lean, the clip's WAV and the key from the
  host). -/
  | upload (method url : String) (headers : List (String × String)) (secret : Option Secret)
      (body : List Part) (timeoutMs : Nat)
  /-- The host may drop the clip's samples. -/
  | forgetClip (clip : Nat)
  /-- Open `target` with its default app (the Finder for a folder, the default editor for a
  text file, System Settings for its URLs): a path (`~/` is the home folder) or a URL with a
  scheme. -/
  | openItem (target : String)
  /-- Whether an app with this bundle identifier is running. -/
  | appRunning (bundleId : String)
  /-- The value of `key` in the defaults domain `domain` (`defaults read domain key`), as UTF-8
  text: a string as it is, a number or a boolean as its text (booleans as `1` or `0`). -/
  | readDefault (domain key : String)
  /-- Create the directory and its missing parents, each private (mode 700); `done` if it is
  already a directory. -/
  | makeDir (path : String)
  /-- Load the image at `source` (a file path, `~/` for the home folder, or an `http`/`https`
  URL) and answer its size in pixels (`Reply.image`); the host keeps the decoded pixels under
  `source` and paints them for `Style.image`s that name it. Lean never sees the pixels. An image
  the host already holds is answered from what it holds, unless `reload`, which reads `source`
  again. -/
  | loadImage (source : String) (reload : Bool)
  /-- Delete the Keychain item `account` (`Secret.Source.keychain`): `done`, also when there is
  none. -/
  | forgetSecret (account : String)
deriving Repr, BEq, Inhabited

inductive Reply where
  /-- `writeFile`, `appendFile`, `deleteFile`, `makeDir`, `forgetSecret` and `playSound`
  succeeded. -/
  | done
  /-- `readFile`'s contents, or `readDefault`'s value. -/
  | bytes (data : ByteArray)
  /-- An HTTP response, whatever its status. -/
  | http (status : Nat) (headers : List (String × String)) (body : ByteArray)
  /-- Any request can fail. -/
  | failed (fault : Fault) (message : String)
  /-- `listDir`'s names. -/
  | names (names : List String)
  /-- `frontmostApp`'s process id and name (empty when it has none). -/
  | app (pid : Nat) (name : String)
  /-- `permission`'s or `appRunning`'s answer. -/
  | flag (granted : Bool)
  /-- `loadImage`'s answer: the image's size in pixels (after its orientation is applied). -/
  | image (width height : Nat)
deriving Repr, BEq, Inhabited

/-- Whether a reply has the shape that answers a request of kind `k`. -/
def Reply.answers : Request.Kind → Reply → Bool
  | _, .failed .. => true
  | .readFile, .bytes _ => true
  | .writeFile, .done | .playSound, .done | .appendFile, .done | .deleteFile, .done => true
  | .typeText, .done | .forgetClip, .done | .openItem, .done | .makeDir, .done => true
  | .forgetSecret, .done => true
  | .readDefault, .bytes _ => true
  | .http, .http .. | .upload, .http .. => true
  | .listDir, .names _ => true
  | .frontmostApp, .app .. => true
  | .permission, .flag _ | .appRunning, .flag _ => true
  | .loadImage, .image .. => true
  | _, _ => false

/-- An outside input an app asks for, as data derived from its state. -/
inductive Sub where
  /-- A tick every `ms` milliseconds (at least 1), from the host. -/
  | every (ms : Nat)
  /-- `changed` whenever the file at `path` changes: written, replaced, created or removed. -/
  | watchFile (path : String)
  /-- Record `clip` from the microphone while active: `started` once the microphone is running,
  then `audio`; or `failed` if it can't start. Stopping it stops the microphone. The host keeps
  the samples for `Part.wav`. Needs Microphone. -/
  | record (clip : Nat)
  /-- The key with virtual key code `code` (with `modifier`, the `NSEvent.ModifierFlags` bit
  that tells a modifier key's press from its release): `keyDown`, `keyUp`, and `otherKey` for
  any other key pressed while it is down. Needs Accessibility. -/
  | globalKey (code : Nat) (modifier : Option Nat)
  /-- Keep the host's decoded images (`Request.loadImage`) within about `bytes` bytes of pixels
  while active: past it the host drops the images used least recently, never one the latest
  frame draws nor the one it just loaded, and reports each with `evicted` (^1011). Without it
  the host keeps every image. The smallest budget of those active wins. -/
  | imageCache (bytes : Nat)
deriving Repr, DecidableEq, Inhabited

def machine : Machine State := { init := {}, moves := moves%, receive }

structure App (S : Type) where
  init : S
  /-- What the app shows: at most one window (a later window is ignored), panels and status
  items. An app with no window is an accessory app (no Dock icon, no main menu). -/
  surfaces : List (Surface S)
  /-- A person's moves: every action names a control on screen. -/
  update : S → Action → S × List Effect
  /-- The outside world: the clock, timers, replies and subscription events
  (docs/effects.md). Ignored by default. -/
  receive : S → Msg → S × List Effect := fun s _ => (s, [])
  /-- The outside inputs the app wants in this state. The runtime diffs them after every
  delivery and starts and stops subscriptions to match. -/
  subscriptions : S → List Sub := fun _ => []
  /-- Effects to run once, when the first clock arrives (so timers start from a real time). -/
  initEffects : List Effect := []
  /-- Every claim the app makes, from the claim commands. -/
  claims : List ClaimInfo
  /-- The control that has keyboard focus at launch, if it is focusable there. -/
  initFocus : Option ControlRef := none
  /-- How many requests of capped kinds (`Request.Kind.capped`: `http`, `upload`, `loadImage`)
  may be with the host at once (at least 1). The runtime queues the rest (docs/effects.md,
  "Requests in flight"). -/
  maxInFlight : Nat := 6
  /-- The window's smallest content size in this state, in points. The host keeps the window
  at least this big, so a person can't drag it smaller (`NSWindow.contentMinSize`; trusted,
  ^1010), and the view can be proved good at every size from it up (with `Grid.minBox`, for
  instance). `0 × 0`, no minimum, by default. -/
  minSize : S → Size := fun _ => ⟨0, 0⟩
  /-- The scroll boxes and virtual lists (by `Style.scrollRef`) whose offset, and what the
  runtime knows of their rows, outlive their leaving the view in this state: a list on a tab not
  shown comes back where it was. Any other box's offset is forgotten when it leaves the tree
  (docs/runtime.md, "Scrolling"). None by default. -/
  keepScroll : S → List ControlRef := fun _ => []