src/Waylean.lean


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

import Wayland

open Wayland Protocols

structure State where
  shmName : Option UInt32 := .none

def requireGlobal (name : String) : Option UInt32 → DisplayM State UInt32
  | .some global => pure global
  | .none        => DisplayM.liftIO <| throw (.userError s!"Missing required global {name}")

def launch : DisplayM State Unit := do
  _ ← DisplayM.registerSignal .SIGINT do
    DisplayM.liftIO (IO.println "Received SIGINT")
    DisplayM.requestQuit
  let disp ← DisplayM.getDisplay
  let registry ← disp.getRegistry
  registry.listen fun
    | .global name "wl_shm" _ => do
        DisplayM.liftIO (IO.println s!"shm global registerd ({name})")
        set ({ shmName := name } : State)
    | _ => pure ()
  disp.sync do
    DisplayM.liftIO (IO.println "Roundtrip complete")
    let shmName ← (← get).shmName |> requireGlobal "wl_shm"
    let shm : WlShm ← registry.bind shmName
    shm.release

def main : IO Unit :=
  DisplayM.run launch { }