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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50

import Wayland
import Waylean.Registry
import Std.Data.HashMap

open Wayland Protocols Waylean

structure Output where
  removed : Bool

structure State where
  registry : Registry.State := .new
  outputs : Std.HashMap RiverOutputV1 Output := { }

structure Context where
  wm : RiverWindowManagerV1
  xkbBindings : RiverXkbBindingsV1

abbrev WindowManagerM (σ : Type) := ReaderT Context (DisplayM σ)

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

def handle (ctx : Context) : RiverWindowManagerV1.Event → DisplayM State Unit
  | .unavailable => do
      DisplayM.liftIO <| IO.println "Another window manager is already running"
      DisplayM.requestQuit
  | .finished => do
      DisplayM.requestQuit
  | .manageStart => do
      let (removedOutputs, aliveOutputs) := (← get).outputs.partition (Function.const _ Output.removed)
      pure ()
  | .renderStart => pure ()
  | .sessionLocked => pure ()
  | .sessionUnlocked => pure ()
  | .window win => pure ()
  | .output out => pure ()
  | .seat seat => pure ()

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 wm : RiverWindowManagerV1 ← zoomRegistry Registry.bindSingleton
    let xkbBindings : RiverXkbBindingsV1 ← zoomRegistry Registry.bindSingleton
    wm.listen (handle { wm, xkbBindings })

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