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
31
32

import Wayland
open Wayland Protocols

def Wayland.Protocols.WlDisplay.roundtrip {σ : Type} (display : WlDisplay) (handler : DisplayM σ Unit) : DisplayM σ Unit := do
  let callback ← display.sync
  callback.listen fun
    | .done _ => do
      callback.keep
      handler

structure State where
  count : Int

partial def nextTimer : DisplayM Int Unit := do
  _ ← DisplayM.registerTimer 16ms do
    let newCount := (← get) + 1
    set newCount
    DisplayM.liftIO (IO.println s!"Timer tick {newCount}")
    nextTimer

def launch : DisplayM State Unit := do
  _ ← DisplayM.registerSignal .SIGINT do
    DisplayM.liftIO (IO.println "Received SIGINT")
    DisplayM.requestQuit
  DisplayM.zoom (mk_lens count) nextTimer

  let disp : WlDisplay ← DisplayM.getDisplay
  disp.roundtrip do
    DisplayM.liftIO (IO.println "Roundtrip complete")

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