From dab858e92dfa5705d1aef7259e03b25747372d95 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Fri, 10 Apr 2026 17:36:15 +0200
Subject: implement registry wrapper

---
 src/Waylean.lean          | 25 ++++++---------
 src/Waylean/Registry.lean | 80 +++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 89 insertions(+), 16 deletions(-)
 create mode 100644 src/Waylean/Registry.lean

(limited to 'src')

diff --git a/src/Waylean.lean b/src/Waylean.lean
index 953096a..47f9db9 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -1,29 +1,22 @@
 import Wayland
+import Waylean.Registry
 
-open Wayland Protocols
+open Wayland Protocols Waylean
 
 structure State where
-  shmName : Option UInt32 := .none
+  registry : Registry.State := .new
 
-def requireGlobal (name : String) : Option UInt32 → DisplayM State UInt32
-  | .some global => pure global
-  | .none        => DisplayM.liftIO <| throw (.userError s!"Missing required global {name}")
+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
-  let disp ← DisplayM.getDisplay
-  let registry ← disp.getRegistry
-  registry.listen fun
-    | .global name "wl_shm" _ => do
-        DisplayM.liftIO (IO.println s!"shm global registerd ({name})")
-        set ({ shmName := name } : State)
-    | _ => pure ()
-  disp.sync do
-    DisplayM.liftIO (IO.println "Roundtrip complete")
-    let shmName ← (← get).shmName |> requireGlobal "wl_shm"
-    let shm : WlShm ← registry.bind shmName
+
+  zoomRegistry Registry.init
+  DisplayM.sync do
+    let shm : WlShm ← zoomRegistry Registry.bindSingleton
     shm.release
 
 def main : IO Unit :=
diff --git a/src/Waylean/Registry.lean b/src/Waylean/Registry.lean
new file mode 100644
index 0000000..378b6dc
--- /dev/null
+++ b/src/Waylean/Registry.lean
@@ -0,0 +1,80 @@
+import Wayland
+import Std.Data.HashMap
+
+open Wayland Protocols
+
+namespace Waylean
+
+set_option linter.unusedVariables false
+def Global (ι : InterfaceName) : Type := UInt32
+  deriving BEq
+set_option linter.unusedVariables true
+
+variable {ι : InterfaceName} [ResolvedInterface ι]
+
+namespace Registry
+
+private structure GlobalInfo where
+  ι : InterfaceName
+  name : Global ι
+  version : UInt32
+
+structure State where
+  private globals : Array GlobalInfo := #[]
+  private registry : Option WlRegistry := .none
+
+def State.new : State := {}
+
+/-- Initialize the registry and start observing globals. -/
+def init : DisplayM State Unit := do
+  let registry ← DisplayM.getRegistry
+  set ({ registry } : State)
+  registry.listen fun
+  | .global name iface version => do
+    let s ← get
+    set { s with
+      globals := s.globals ++ #[
+        ({ ι := iface, name, version } : GlobalInfo)
+      ]
+    }
+  | .globalRemove name => do
+    let s ← get
+    set { s with
+      globals := s.globals.filter fun info ↦
+        info.name != name
+    }
+
+/-- Get a list of globals for a certain interface type. -/
+def getGlobals : DisplayM State (Array (Global ι)) := do
+  let minVersion := (inferInstance : Interface ι).version
+  let globals := (← get).globals
+  return globals.filterMap fun g ↦
+    if g.ι == ι && g.version >= minVersion
+    then .some g.name
+    else .none
+
+/-- Get a singleton instance for a global of a certain interface type. -/
+def getSingleton? : DisplayM State (Option (Global ι)) := do
+  match (← getGlobals) with
+    | #[g] => pure (.some g)
+    | _    => pure .none
+
+/-- Require a singleton instance for a global of a certain interface type. -/
+def requireSingleton : DisplayM State (Global ι) := do
+  match (← getSingleton?) with
+    | .some g => pure g
+    | .none   => throw (.userError s!"No singleton instance for interface {ι}")
+
+end Registry
+
+/-- Bind a global instance. -/
+def Global.bind (global : Global ι) : DisplayM Registry.State (Object ι) := do
+  let registry ← (← get).registry
+    |>.map pure
+    |>.getD (throw (.userError "Registry not initialized"))
+  registry.bind global
+
+def Registry.bindSingleton : DisplayM Registry.State (Object ι) := do
+  (← requireSingleton).bind
+
+end Waylean
-- 
cgit v1.3.1