1 files changed, 80 insertions, 0 deletions
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