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

import Wayland
import Waylean.Registry

open Wayland Protocols Waylean

structure State where
  registry : Registry.State := .new

def zoomRegistry {α : Type} : DisplayM Registry.State α → DisplayM State α :=
  DisplayM.zoom (mk_lens registry)

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

  zoomRegistry Registry.init
  DisplayM.sync do
    let shm : WlShm ← zoomRegistry Registry.bindSingleton
    shm.release

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