6 files changed, 109 insertions, 25 deletions
diff --git a/lakefile.lean b/lakefile.lean
index 271a216..512912d 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -53,6 +53,10 @@ lean_lib «Wayland» where
   roots := #[`Wayland]
   extraDepTargets := #[`WaylandProtocolsSources]
 
+lean_lib «WayleanLib» where
+  srcDir := "src"
+  roots := #[`Waylean]
+
 lean_exe «Waylean» where
   srcDir := "src"
   root := `Waylean
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 63bd70d..704d7d4 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -21,7 +21,7 @@ section Interfaces
 /-- The name of an interface (e.g., `"wl_display"`), commonly used to resolve the corresponding interface description
 using the `Interface` class. -/
 def InterfaceName : Type := String
-  deriving Repr, Nonempty, BEq, ToString
+  deriving Repr, Nonempty, BEq, ToString, Hashable
 
 /-- The numeric identifier of a request/event in an interface. -/
 def OpCode : Type := UInt32
@@ -145,6 +145,7 @@ def DisplayM (σ : Type) : Type → Type :=
 
 deriving instance Monad for DisplayM σ
 deriving instance MonadState σ for DisplayM σ
+deriving instance MonadExcept IO.Error for DisplayM σ
 
 private instance : MonadLift (ReaderT (Display σ) (StateT σ IO)) (DisplayM σ) where
   monadLift := id
diff --git a/lib/Wayland/Helpers.lean b/lib/Wayland/Helpers.lean
index 7230fc2..71d02d5 100644
--- a/lib/Wayland/Helpers.lean
+++ b/lib/Wayland/Helpers.lean
@@ -12,4 +12,10 @@ variable {σ : Type}
 /-- Get the `wl_display` instance within the display monad. -/
 def DisplayM.getDisplay : DisplayM σ WlDisplay := getDisplay'
 
+def DisplayM.sync (done : DisplayM σ Unit) : DisplayM σ Unit := do
+  (← getDisplay).sync done
+
+def DisplayM.getRegistry : DisplayM σ WlRegistry := do
+  (← getDisplay).getRegistry
+
 end Wayland
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
diff --git a/tools/Scanner/Parser.lean b/tools/Scanner/Parser.lean
index 7b64822..bb89648 100644
--- a/tools/Scanner/Parser.lean
+++ b/tools/Scanner/Parser.lean
@@ -44,16 +44,16 @@ private def Element.textContent (el : Xml.Element) : String :=
     |> String.intercalate "\n"
     |>.trimAscii
     |>.toString
-  reformat <| String.join <| Array.toList <| el.content.flatMap fun
-    | .Element _ => #[]
-    | .Comment _ => #[]
-    | .Character s => #[s]
+  reformat <| String.join <| Array.toList <| el.content.filterMap fun
+    | .Element _ => .none
+    | .Comment _ => .none
+    | .Character s => .some s
 
 private def Element.getChildrenByName (el : Xml.Element) (name : String) : Array Xml.Element :=
-  el.content.flatMap fun
-    | .Element child => if child.name == name then #[child] else #[]
-    | .Comment _ => #[]
-    | .Character _ => #[]
+  el.content.filterMap fun
+    | .Element child => if child.name == name then .some child else .none
+    | .Comment _ => .none
+    | .Character _ => .none
 
 private def Element.getChildByName (el : Xml.Element) (name : String) : Option Xml.Element :=
   match el.getChildrenByName name with