src/Waylean.lean


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

import Wayland
open Wayland

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

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