wip tinyrwm in lean

9 files changed, 460 insertions, 97 deletions

diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc
index f3c966c..08df50b 100644
--- a/lib/CWayland/CWayland.cc
+++ b/lib/CWayland/CWayland.cc
@@ -1299,17 +1299,9 @@ lean_obj_res waylean_proxy_get_type(b_lean_obj_arg proxy_obj)
     return lean_io_result_mk_ok(lean_mk_string(name));
 }
 
-// Proxy.isEqual : (x y : @& Proxy) → Bool
-lean_obj_res waylean_proxy_is_equal(b_lean_obj_arg x, b_lean_obj_arg y)
-{
-    auto x_proxy = static_cast<wl_proxy*>(lean_get_external_data(x));
-    auto y_proxy = static_cast<wl_proxy*>(lean_get_external_data(y));
-    return lean_box(x_proxy == y_proxy ? 1 : 0);
-}
-
-// Proxy.hash : (x : @& Proxy) → UInt64
-lean_obj_res waylean_proxy_hash(b_lean_obj_arg x)
+// Proxy.getID : (x : @& Proxy) → IO UInt64
+lean_obj_res waylean_proxy_get_id(b_lean_obj_arg x)
 {
     auto proxy = static_cast<wl_proxy*>(lean_get_external_data(x));
-    return lean_box_uint64(wl_proxy_get_id(proxy));
+    return lean_io_result_mk_ok(lean_box_uint64(wl_proxy_get_id(proxy)));
 }
\ No newline at end of file
diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h
index e4a6897..ff71348 100644
--- a/lib/CWayland/CWayland.h
+++ b/lib/CWayland/CWayland.h
@@ -83,9 +83,7 @@ lean_obj_res waylean_proxy_listen          (b_lean_obj_arg proxy,
                                             lean_obj_arg   handler);
 lean_obj_res waylean_proxy_keep            (b_lean_obj_arg proxy);
 lean_obj_res waylean_proxy_get_type        (b_lean_obj_arg proxy);
-lean_obj_res waylean_proxy_is_equal        (b_lean_obj_arg x,
-                                            b_lean_obj_arg y);
-lean_obj_res waylean_proxy_hash            (b_lean_obj_arg x);
+lean_obj_res waylean_proxy_get_id          (b_lean_obj_arg x);
 
 #ifdef __cplusplus
 }
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 3cfa679..d82a951 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -34,12 +34,14 @@ def Fd : Type := Int32
 /-- Handle to a client object, possibly dead. -/
 structure Object (ι : InterfaceName) : Type where
   private proxy : Native.Proxy
+  private id : UInt64
   deriving Nonempty
 
 /-- Opaque handle to an object whose type is not statically known. -/
 structure AnyObject : Type where
   private proxy : Native.Proxy
   private type : String
+  private id : UInt64
   deriving Nonempty
 
 /-- Monad in which arguments can be marshalled one after another. -/
@@ -278,11 +280,12 @@ private instance : ArgumentDemarshaller (ExceptT String ArgumentBufferM) where
   demarshalString := do (← read).readString
   demarshalObject := do
     let proxy ← (← read).readObject
-    return proxy.map Object.mk
+    proxy.mapM fun proxy ↦ do
+      return ⟨proxy, ← proxy.getID⟩
   demarshalAnyObject := do
     let proxy ← (← read).readObject
     proxy.mapM fun proxy ↦ do
-      return ⟨proxy, ← proxy.getType⟩
+      return ⟨proxy, ← proxy.getType, ← proxy.getID⟩
   demarshalArray := do (← read).readArray
   demarshalFd := do (← read).readFd
 
@@ -412,21 +415,21 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter
 
 def DisplayM.getDisplay' : DisplayM σ (Object "wl_display") := do
   let proxy ← Native.Proxy.fromDisplay (← read).disp
-  return ⟨proxy⟩
+  return ⟨proxy, ← proxy.getID⟩
 
 variable {ι ι' : InterfaceName}
 
 instance : BEq (Object ι) where
-  beq x y := x.proxy.isEqual y.proxy
+  beq x y := x.id == y.id
 
 instance : Hashable (Object ι) where
-  hash x := x.proxy.hash
+  hash x := x.id
 
 instance : BEq AnyObject where
-  beq x y := x.proxy.isEqual y.proxy
+  beq x y := x.id == y.id
 
 instance : Hashable AnyObject where
-  hash x := x.proxy.hash
+  hash x := x.id
 
 private def marshalArguments (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : IO (Native.ArgumentBuffer × OpCode) := do
   let argBuffer ← Native.ArgumentBuffer.new
@@ -445,7 +448,7 @@ def Object.sendConstructor [iface : ResolvedInterface ι'] (obj : Object ι) (ma
   let typeMap := (← read).typeMap
   let (argBuffer, opcode) ← marshalArguments marshaller
   let proxy ← obj.proxy.sendConstructor opcode argBuffer typeMap ι'
-  return ⟨proxy⟩
+  return ⟨proxy, ← proxy.getID⟩
 
 /-- Listen for events from the server for an object. -/
 def Object.listen [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := do
@@ -462,11 +465,11 @@ def Object.keep (obj : Object ι) : DisplayM σ Unit :=
 
 /-- Erase the type information from an object. -/
 def Object.toAny (obj : Object ι) : AnyObject :=
-  ⟨obj.proxy, ι⟩
+  ⟨obj.proxy, ι, obj.id⟩
 
 /-- Try to cast a type-erased object into a typed object. -/
 def AnyObject.cast (obj : AnyObject) : Option (Object ι) :=
-  if obj.type == ι then .some ⟨obj.proxy⟩ else .none
+  if obj.type == ι then .some ⟨obj.proxy, obj.id⟩ else .none
 
 end Proxies
 
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index 601c709..72b0cf2 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -142,10 +142,7 @@ opaque Proxy.keep : (proxy : @& Proxy) → IO Unit
 @[extern "waylean_proxy_get_type"]
 opaque Proxy.getType : (proxy : @& Proxy) → IO String
 
-@[extern "waylean_proxy_is_equal"]
-opaque Proxy.isEqual : (x y : @& Proxy) → Bool
-
-@[extern "waylean_proxy_hash"]
-opaque Proxy.hash : (x : @& Proxy) → UInt64
+@[extern "waylean_proxy_get_id"]
+opaque Proxy.getID : (x : @& Proxy) → IO UInt64
 
 end Wayland.Native
diff --git a/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean b/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean
index 3f62b69..48f22dc 100644
--- a/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean
+++ b/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean
@@ -20,9 +20,9 @@ inductive RiverLibinputDeviceV1.Error where
   | invalidArg
 
 structure RiverLibinputDeviceV1.SendEventsModes where
-  enabled : Bool
-  disabled : Bool
-  disabledOnExternalMouse : Bool
+  enabled : Bool := false
+  disabled : Bool := false
+  disabledOnExternalMouse : Bool := false
 
 inductive RiverLibinputDeviceV1.TapState where
   | disabled
@@ -53,10 +53,10 @@ inductive RiverLibinputDeviceV1.AccelProfile where
   | custom
 
 structure RiverLibinputDeviceV1.AccelProfiles where
-  none : Bool
-  flat : Bool
-  adaptive : Bool
-  custom : Bool
+  none : Bool := false
+  flat : Bool := false
+  adaptive : Bool := false
+  custom : Bool := false
 
 inductive RiverLibinputDeviceV1.NaturalScrollState where
   | disabled
@@ -72,9 +72,9 @@ inductive RiverLibinputDeviceV1.ClickMethod where
   | clickfinger
 
 structure RiverLibinputDeviceV1.ClickMethods where
-  none : Bool
-  buttonAreas : Bool
-  clickfinger : Bool
+  none : Bool := false
+  buttonAreas : Bool := false
+  clickfinger : Bool := false
 
 inductive RiverLibinputDeviceV1.ClickfingerButtonMap where
   | lrm
@@ -91,10 +91,10 @@ inductive RiverLibinputDeviceV1.ScrollMethod where
   | onButtonDown
 
 structure RiverLibinputDeviceV1.ScrollMethods where
-  noScroll : Bool
-  twoFinger : Bool
-  edge : Bool
-  onButtonDown : Bool
+  noScroll : Bool := false
+  twoFinger : Bool := false
+  edge : Bool := false
+  onButtonDown : Bool := false
 
 inductive RiverLibinputDeviceV1.ScrollButtonLockState where
   | disabled
diff --git a/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean b/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean
index 4acaf02..4da96e7 100644
--- a/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean
+++ b/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean
@@ -38,17 +38,17 @@ inductive RiverWindowV1.DecorationHint where
   | noPreference
 
 structure RiverWindowV1.Edges where
-  none : Bool
-  top : Bool
-  bottom : Bool
-  left : Bool
-  right : Bool
+  none : Bool := false
+  top : Bool := false
+  bottom : Bool := false
+  left : Bool := false
+  right : Bool := false
 
 structure RiverWindowV1.Capabilities where
-  windowMenu : Bool
-  maximize : Bool
-  fullscreen : Bool
-  minimize : Bool
+  windowMenu : Bool := false
+  maximize : Bool := false
+  fullscreen : Bool := false
+  minimize : Bool := false
 
 inductive RiverDecorationV1.Error where
   | noCommit
@@ -65,13 +65,13 @@ inductive RiverOutputV1.PresentationMode where
   | async
 
 structure RiverSeatV1.Modifiers where
-  none : Bool
-  shift : Bool
-  ctrl : Bool
-  mod1 : Bool
-  mod3 : Bool
-  mod4 : Bool
-  mod5 : Bool
+  none : Bool := false
+  shift : Bool := false
+  ctrl : Bool := false
+  mod1 : Bool := false
+  mod3 : Bool := false
+  mod4 : Bool := false
+  mod5 : Bool := false
 
 namespace RiverWindowManagerV1.Error
 
diff --git a/lib/Wayland/Protocols/Wayland/Header.lean b/lib/Wayland/Protocols/Wayland/Header.lean
index a12c0bf..3d7346d 100644
--- a/lib/Wayland/Protocols/Wayland/Header.lean
+++ b/lib/Wayland/Protocols/Wayland/Header.lean
@@ -201,27 +201,27 @@ inductive WlDataDevice.Error where
   | usedSource
 
 structure WlDataDeviceManager.DndAction where
-  none : Bool
-  copy : Bool
-  move : Bool
-  ask : Bool
+  none : Bool := false
+  copy : Bool := false
+  move : Bool := false
+  ask : Bool := false
 
 inductive WlShell.Error where
   | role
 
 structure WlShellSurface.Resize where
-  none : Bool
-  top : Bool
-  bottom : Bool
-  left : Bool
-  topLeft : Bool
-  bottomLeft : Bool
-  right : Bool
-  topRight : Bool
-  bottomRight : Bool
+  none : Bool := false
+  top : Bool := false
+  bottom : Bool := false
+  left : Bool := false
+  topLeft : Bool := false
+  bottomLeft : Bool := false
+  right : Bool := false
+  topRight : Bool := false
+  bottomRight : Bool := false
 
 structure WlShellSurface.Transient where
-  inactive : Bool
+  inactive : Bool := false
 
 inductive WlShellSurface.FullscreenMethod where
   | default
@@ -237,9 +237,9 @@ inductive WlSurface.Error where
   | defunctRoleObject
 
 structure WlSeat.Capability where
-  pointer : Bool
-  keyboard : Bool
-  touch : Bool
+  pointer : Bool := false
+  keyboard : Bool := false
+  touch : Bool := false
 
 inductive WlSeat.Error where
   | missingCapability
@@ -293,8 +293,8 @@ inductive WlOutput.Transform where
   | flipped270
 
 structure WlOutput.Mode where
-  current : Bool
-  preferred : Bool
+  current : Bool := false
+  preferred : Bool := false
 
 inductive WlSubcompositor.Error where
   | badSurface
diff --git a/src/Waylean.lean b/src/Waylean.lean
index 6334301..0f0a2e1 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -4,39 +4,415 @@ import Std.Data.HashMap
 
 open Wayland Protocols Waylean
 
+def Array.findAndModifyM {α : Type} {m : Type → Type} [Monad m] (a : Array α) (pred : α → Bool) (update : α → m α) : m (Array α × Option α) := do
+  let idx := a.findIdx pred
+  if h : idx < a.size then
+    let new ← update a[idx]
+    return (a.setIfInBounds idx new, new)
+  else return (a, .none)
+
+def Array.findAndModify {α : Type} (a : Array α) (pred : α → Bool) (update : α → α) : Array α × Option α :=
+  (a.findAndModifyM pred (update : α → Id α) : Id (Array α × Option α))
+
+def Std.HashMap.mapM {α β γ : Type} [BEq α] [Hashable α] {m : Type → Type} [Monad m] (map : Std.HashMap α β) (update : α → β → m γ) : m (Std.HashMap α γ) := do
+  let a := map.toArray
+  let a' ← a.mapM fun (x, y) ↦ do return (x, ← update x y)
+  return Std.HashMap.ofArray a'
+
+def Std.HashMap.lens {α β : Type} [BEq α] [Hashable α] (key : α) : Lens (Std.HashMap α β) (Option β) where
+  get x := x.get? key
+  set v x := x.alter key fun _ ↦ v
+
+def Std.HashMap.modifyM {α β : Type} [BEq α] [Hashable α] {m : Type → Type} [Monad m] (map : Std.HashMap α β) (key : α) (update : β → m β) : m (Std.HashMap α β) := do
+  if h : map.contains key then
+    let new ← update (map.get key h)
+    return map.insert key new
+  else return map
+
+inductive Action where
+  | none
+  | spawnFoot
+  | close
+  | focusNext
+  | move
+  | resize
+  | exit
+
+inductive SeatOp where
+  | none
+  | move (window : RiverWindowV1) (startX startY : Int32)
+  | resize (window : RiverWindowV1) (startX startY startWidth startHeight : Int32) (edges : RiverWindowV1.Edges)
+
+structure XkbBinding where
+  proxy : RiverXkbBindingV1
+  action : Action
+
+structure PointerBinding where
+  proxy : RiverPointerBindingV1
+  action : Action
+
+structure Window where
+  proxy : RiverWindowV1
+  node : RiverNodeV1
+  new : Bool := true
+  closed : Bool := false
+  x : Int32 := 0
+  y : Int32 := 0
+  width : Int32 := 0
+  height : Int32 := 0
+  pointerMoveRequested : Option RiverSeatV1 := .none
+  pointerResizeRequested : Option RiverSeatV1 := .none
+  pointerResizeRequestedEdges : RiverWindowV1.Edges := {}
+
 structure Output where
-  removed : Bool
+  proxy : RiverOutputV1
+  removed : Bool := false
+
+structure Seat where
+  proxy : RiverSeatV1
+  new : Bool := true
+  removed : Bool := false
+  focused : Option RiverWindowV1 := .none
+  hovered : Option RiverWindowV1 := .none
+  interacted : Option RiverWindowV1 := .none
+  xkbBindings : Std.HashMap RiverXkbBindingV1 XkbBinding := {}
+  pointerBindings : Std.HashMap RiverPointerBindingV1 PointerBinding := {}
+  pendingAction : Action := .none
+  op : SeatOp := .none
+  opDeltaX : Int32 := 0
+  opDeltaY : Int32 := 0
+  opRelease : Bool := false
 
 structure State where
   registry : Registry.State := .new
-  outputs : Std.HashMap RiverOutputV1 Output := { }
+  windows : Array Window := #[]
+  outputs : Std.HashMap RiverOutputV1 Output := {}
+  seats : Std.HashMap RiverSeatV1 Seat := {}
+
+def zoomRegistry {α : Type} : DisplayM Registry.State α → DisplayM State α := DisplayM.zoom (mk_lens registry)
+
+def handleSeat (ev : RiverSeatV1.Event) : DisplayM (Option Seat) Unit := do
+  for s in ← get do
+    match ev with
+      | .removed               => set (Option.some { s with removed := true })
+      | .pointerEnter win      => set (Option.some { s with hovered := win })
+      | .pointerLeave          => set (Option.some { s with hovered := .none })
+      | .windowInteraction win => set (Option.some { s with interacted := win })
+      | .opDelta x y           => set (Option.some { s with opDeltaX := x, opDeltaY := y })
+      | .opRelease             => set (Option.some { s with opRelease := true })
+      | _                      => pure ()
+
+def handleXkbBinding (proxy : RiverXkbBindingV1) (ev : RiverXkbBindingV1.Event) : DisplayM (Option Seat) Unit := do
+  for s in ← get do
+    for binding in s.xkbBindings.get? proxy do
+      match ev with
+        | .pressed => set (Option.some { s with pendingAction := binding.action })
+        | _        => pure ()
+
+def handlePointerBinding (proxy : RiverPointerBindingV1) (ev : RiverPointerBindingV1.Event) : DisplayM (Option Seat) Unit := do
+  for s in ← get do
+    for binding in s.pointerBindings.get? proxy do
+      match ev with
+        | .pressed => set (Option.some { s with pendingAction := binding.action })
+        | _        => pure ()
+
+def handleOutput (ev : RiverOutputV1.Event) : DisplayM (Option Output) Unit := do
+  for o in ← get do
+    match ev with
+      | .removed => set (Option.some { o with removed := true })
+      | _        => pure ()
+
+def handleWindow (proxy : RiverWindowV1) (ev : RiverWindowV1.Event) : DisplayM State Unit := do
+  let windows := (← get).windows.findAndModify (fun win ↦ win.proxy == proxy) fun win ↦
+    match ev with
+    | .closed                     => { win with closed := true }
+    | .dimensions w h             => { win with width := w, height := h }
+    | .pointerMoveRequested s     => { win with pointerMoveRequested := s }
+    | .pointerResizeRequested s e => { win with pointerResizeRequested := s, pointerResizeRequestedEdges := e }
+    | _                           => win
+  set { ← get with windows := windows.fst }
 
 structure Context where
   wm : RiverWindowManagerV1
   xkbBindings : RiverXkbBindingsV1
 
-abbrev WindowManagerM (σ : Type) := ReaderT Context (DisplayM σ)
+def Window.setPosition {σ : Type} (w : Window) (x y : Int32) : DisplayM σ Window := do
+  w.node.setPosition x y
+  return { w with x, y}
+
+def Seat.createXkbBinding (ctx : Context) (mods : RiverSeatV1.Modifiers) (keysym : UInt32) (action : Action) : DisplayM (Option Seat) Unit := do
+  for s in ← get do
+    let proxy ← ctx.xkbBindings.getXkbBinding s.proxy keysym mods
+    proxy.enable
+    proxy.listen (handleXkbBinding proxy)
+    let xkbBindings := s.xkbBindings.insert proxy { proxy, action }
+    set (Option.some { s with xkbBindings })
+
+def Seat.createPointerBinding (mods : RiverSeatV1.Modifiers) (button : UInt32) (action : Action) : DisplayM (Option Seat) Unit := do
+  for s in ← get do
+    let proxy ← s.proxy.getPointerBinding button mods
+    proxy.enable
+    proxy.listen (handlePointerBinding proxy)
+    let pointerBindings := s.pointerBindings.insert proxy { proxy, action }
+    set (Option.some { s with pointerBindings })
+
+def Seat.pointerMove {σ : Type} (seat : Seat) (win : Window) : DisplayM σ Seat := do
+  seat.proxy.opStartPointer
+  return { seat with
+    interacted := win.proxy
+    op := .move win.proxy win.x win.y
+    opDeltaX := 0
+    opDeltaY := 0
+  }
+
+def Seat.pointerResize {σ : Type} (seat : Seat) (win : Window) (edges : RiverWindowV1.Edges) : DisplayM σ Seat := do
+  seat.proxy.opStartPointer
+  win.proxy.informResizeStart
+  return { seat with
+    interacted := win.proxy
+    op := .resize win.proxy win.x win.y win.width win.height edges
+    opDeltaX := 0
+    opDeltaY := 0
+  }
+
+def Seat.focusTop (s : Seat) : DisplayM State Seat := do
+  let windows := (← get).windows
+  if h : windows.size == 0 then
+    s.proxy.clearFocus
+    return { s with focused := .none }
+  else
+    let win := windows[windows.size - 1]'(by
+      apply Nat.sub_one_lt
+      rw [beq_iff_eq] at h
+      assumption)
+    s.proxy.focusWindow win.proxy
+    win.node.placeTop
+    return { s with focused := win.proxy }
+
+def Seat.doAction (s : Seat) (ctx : Context) : DisplayM State Seat := do
+  let action := s.pendingAction
+  let mut s : Seat := { s with pendingAction := .none }
+  match action with
+    | .none =>
+        pure ()
+    | .spawnFoot =>
+        _ ← DisplayM.liftIO <| IO.Process.spawn {
+          cmd := "foot"
+          env := #[("WAYLAND_DEBUG", .none)]
+        }
+    | .close =>
+        for window in s.focused do
+          window.close
+    | .focusNext =>
+        let mut windows := (← get).windows
+        if h : 0 < windows.size then
+          let win := windows[0]
+          windows := windows.eraseIdx 0
+          windows := windows.push win
+        set { ← get with windows }
+        s ← focusTop s
+    | .move =>
+        for proxy in s.hovered do
+          for win in (← get).windows.find? (fun win ↦ win.proxy == proxy) do
+            s ← s.pointerMove win
+    | .resize =>
+        for proxy in s.hovered do
+          for win in (← get).windows.find? (fun win ↦ win.proxy == proxy) do
+            s ← s.pointerResize win { bottom := true, right := true }
+    | .exit =>
+        ctx.wm.exitSession
+  return s
+
+def Seat.opEnd (s : Seat) : DisplayM State Seat := do
+  match s.op with
+    | .resize proxy _ _ _ _ _ => proxy.informResizeEnd
+    | _ => pure ()
+  s.proxy.opEnd
+  return { s with op := .none }
+
+def Seat.opManage (s : Seat) : DisplayM State Seat := do
+  match s.op with
+    | .resize proxy startX startY startWidth startHeight edges =>
+        let mut width := startWidth
+        let mut height := startHeight
+        if edges.left   then width  := width  - s.opDeltaX
+        if edges.right  then width  := width  + s.opDeltaX
+        if edges.top    then height := height - s.opDeltaY
+        if edges.bottom then height := height + s.opDeltaY
+        proxy.proposeDimensions width height
+        pure { s with op := .resize proxy startX startY width height edges }
+    | _ => pure s
+
+def removeOutputs : DisplayM State Unit := do
+  let (removedOutputs, aliveOutputs) := (← get).outputs.partition fun _ out ↦ out.removed
+  for out in removedOutputs.values do
+    out.proxy.destroy
+  set { ← get with outputs := aliveOutputs }
+
+def removeWindows : DisplayM State Unit := do
+  let (closedWindows, aliveWindows) := (← get).windows.partition Window.closed
+  let mut seats := (← get).seats
+  for win in closedWindows do
+    seats ← seats.mapM fun _ seat ↦ do
+      let op  ← match seat.op with
+        | .none => pure SeatOp.none
+        | .move proxy startX startY =>
+            if proxy == win.proxy then
+              seat.proxy.opEnd
+              pure SeatOp.none
+            else pure (SeatOp.move proxy startX startY)
+        | .resize proxy startX startY startWidth startHeight edges =>
+            if proxy == win.proxy then
+              seat.proxy.opEnd
+              pure SeatOp.none
+            else pure (SeatOp.resize proxy startX startY startWidth startHeight edges)
+      pure { seat with
+        op
+        focused := if seat.focused == win.proxy then .none else seat.focused
+        hovered := if seat.hovered == win.proxy then .none else seat.hovered
+        interacted := if seat.interacted == win.proxy then .none else seat.interacted
+      }
+    win.proxy.destroy
+  set { ← get with windows := aliveWindows, seats }
+
+def removeSeats : DisplayM State Unit := do
+  let (removedSeats, aliveSeats) := (← get).seats.partition fun _ seat ↦ seat.removed
+  for seat in removedSeats.values do
+    for binding in seat.xkbBindings.values do
+      binding.proxy.destroy
+    for binding in seat.pointerBindings.values do
+      binding.proxy.destroy
+    seat.proxy.destroy
+  set { ← get with seats := aliveSeats }
+
+def initNewWindows : DisplayM State Unit := do
+  let windows ← (← get).windows.mapM fun win ↦ do
+    let mut win := win
+    if win.new then
+      win ← win.setPosition win.x win.y
+      win.proxy.proposeDimensions win.width win.height
+      win := { win with new := false }
+    pure win
+  set { ← get with windows }
+
+def initNewSeats (ctx : Context) : DisplayM State Unit := do
+  -- See xkbcommon/xkbcommon-keysyms.h
+  let space : UInt32 := 0x20
+  let n : UInt32 := 0x6e
+  let q : UInt32 := 0x71
+  let esc : UInt32 := 0xff1b
+  -- See linux/input-event-codes.h
+  let btnLeft : UInt32 := 0x110
+  let btnRight : UInt32 := 0x111
+  let mods : RiverSeatV1.Modifiers := { mod1 := true }
+
+  for s in (← get).seats.values.filter Seat.new do
+    DisplayM.zoom (mk_lens seats) do
+      DisplayM.zoom (Std.HashMap.lens s.proxy) do
+        set (Option.some { s with new := false })
+        Seat.createXkbBinding ctx mods space .spawnFoot
+        Seat.createXkbBinding ctx mods q .close
+        Seat.createXkbBinding ctx mods n .focusNext
+        Seat.createXkbBinding ctx mods esc .exit
+        Seat.createPointerBinding mods btnLeft .move
+        Seat.createPointerBinding mods btnRight .resize
+
+def manageWindows : DisplayM State Unit := do
+  let windows ← (← get).windows.mapM fun win ↦ do
+    let mut seats := (← get).seats
+    for proxy in win.pointerMoveRequested do
+      seats ← seats.modifyM proxy (fun s ↦ s.pointerMove win)
+    for proxy in win.pointerResizeRequested do
+      seats ← seats.modifyM proxy (fun s ↦ s.pointerResize win win.pointerResizeRequestedEdges)
+    set { ← get with seats }
+    pure { win with
+      pointerMoveRequested := .none
+      pointerResizeRequested := .none
+    }
+  set { ← get with windows }
 
-def zoomRegistry {α : Type} : DisplayM Registry.State α → DisplayM State α :=
-  DisplayM.zoom (mk_lens registry)
+def manageSeats (ctx : Context) : DisplayM State Unit := do
+  let seats ← (← get).seats.mapM fun _ seat ↦ do
+    for proxy in seat.interacted do
+      let mut windows := (← get).windows
+      let winIdx := windows.findIdx (fun win ↦ win.proxy == proxy)
+      if h : winIdx < windows.size then
+        let win := windows[winIdx]
+        windows := windows.eraseIdx winIdx
+        windows := windows.push win
+      set { ← get with windows }
+    let mut seat := seat
+    seat ← seat.focusTop
+    seat ← seat.doAction ctx
+    if seat.opRelease then
+      seat ← seat.opEnd
+    else
+      seat ← seat.opManage
+    pure { seat with
+      interacted := .none
+      opRelease := false
+    }
+  set { ← get with seats }
 
 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
-      IO.println "Finished"
       DisplayM.requestQuit
   | .manageStart => do
-      IO.println "Manage Start"
-      let (removedOutputs, aliveOutputs) := (← get).outputs.partition (Function.const _ Output.removed)
-      pure ()
-  | .renderStart => pure ()
+      removeOutputs
+      removeWindows
+      removeSeats
+      initNewWindows
+      initNewSeats ctx
+      manageWindows
+      manageSeats ctx
+      ctx.wm.manageFinish
+  | .renderStart => do
+      let seats ←  (← get).seats.mapM fun _ seat ↦ do
+        match seat.op with
+          | .none => pure seat
+          | .move proxy startX startY =>
+              let windows ← (← get).windows.findAndModifyM
+                (fun win ↦ win.proxy == proxy)
+                (fun win ↦ win.setPosition (startX + seat.opDeltaX) (startY + seat.opDeltaY))
+              set { ← get with windows := windows.fst }
+              pure seat
+          | .resize proxy startX startY startWidth startHeight edges =>
+              let windows ← (← get).windows.findAndModifyM
+                (fun win ↦ win.proxy == proxy)
+                (fun win ↦
+                  let x := startX + if edges.left then (startWidth - win.width) else 0
+                  let y := startY + if edges.top then (startHeight - win.height) else 0
+                  win.setPosition x y)
+              set { ← get with windows := windows.fst }
+              match windows.snd with
+                | .none => pure seat
+                | .some win => pure { seat with op := .resize proxy win.x win.y startWidth startHeight edges }
+      set { ← get with seats }
+      ctx.wm.renderFinish
   | .sessionLocked => pure ()
   | .sessionUnlocked => pure ()
-  | .window win => pure ()
-  | .output out => pure ()
-  | .seat seat => pure ()
+  | .window proxy => do
+      let windows := (← get).windows.push {
+        proxy
+        node := ← proxy.getNode
+      }
+      set { ← get with windows }
+      proxy.listen (handleWindow proxy)
+  | .output proxy => do
+      let outputs := (← get).outputs.insert proxy { proxy }
+      set { ← get with outputs }
+      DisplayM.zoom (mk_lens outputs) do
+        DisplayM.zoom (Std.HashMap.lens proxy) do
+          proxy.listen handleOutput
+  | .seat proxy => do
+      let seats := (← get).seats.insert proxy { proxy }
+      set { ← get with seats }
+      DisplayM.zoom (mk_lens seats) do
+        DisplayM.zoom (Std.HashMap.lens proxy) do
+          proxy.listen handleSeat
 
 def launch : DisplayM State Unit := do
   _ ← DisplayM.registerSignal .SIGINT do
@@ -46,10 +422,7 @@ def launch : DisplayM State Unit := do
   DisplayM.sync do
     let wm : RiverWindowManagerV1 ← zoomRegistry Registry.bindSingleton
     let xkbBindings : RiverXkbBindingsV1 ← zoomRegistry Registry.bindSingleton
-    wm.listen fun ev ↦ do
-      wm.keep
-      xkbBindings.keep
-      handle { wm, xkbBindings } ev
+    wm.listen (handle { wm, xkbBindings })
 
 def main : IO Unit :=
-  DisplayM.run launch { } (name := "wayland-2")
+  DisplayM.run launch { }
diff --git a/tools/Scanner/Generator.lean b/tools/Scanner/Generator.lean
index dc4a87f..2fa4fdd 100644
--- a/tools/Scanner/Generator.lean
+++ b/tools/Scanner/Generator.lean
@@ -112,7 +112,7 @@ private def emitEnumDefinitions (protocol : ProtocolDesc) : Generator Unit := do
       if enum.bitfield then
         emitLine s!"structure {iface.name.pascalCase}.{enum.name.pascalCase} where"
         for entry in enum.entries do
-          emitLine s!"  {entry.name.camelCase} : Bool"
+          emitLine s!"  {entry.name.camelCase} : Bool := false"
       else
         emitLine s!"inductive {iface.name.pascalCase}.{enum.name.pascalCase} where"
         for entry in enum.entries do