From 350d3ca21e6a2d215016c84afa07ccb75abd8a6e Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Fri, 5 Jun 2026 17:04:51 +0200 Subject: wip tinyrwm in lean --- src/Waylean.lean | 409 ++++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 391 insertions(+), 18 deletions(-) (limited to 'src') 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 { } -- cgit v1.3.1