diff options
| -rw-r--r-- | lib/CWayland/CWayland.cc | 14 | ||||
| -rw-r--r-- | lib/CWayland/CWayland.h | 4 | ||||
| -rw-r--r-- | lib/Wayland/Display.lean | 23 | ||||
| -rw-r--r-- | lib/Wayland/Native.lean | 7 | ||||
| -rw-r--r-- | lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean | 28 | ||||
| -rw-r--r-- | lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean | 32 | ||||
| -rw-r--r-- | lib/Wayland/Protocols/Wayland/Header.lean | 38 | ||||
| -rw-r--r-- | src/Waylean.lean | 409 | ||||
| -rw-r--r-- | tools/Scanner/Generator.lean | 2 |
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 |