From dab858e92dfa5705d1aef7259e03b25747372d95 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Fri, 10 Apr 2026 17:36:15 +0200 Subject: implement registry wrapper --- lib/Wayland/Display.lean | 3 ++- lib/Wayland/Helpers.lean | 6 ++++++ 2 files changed, 8 insertions(+), 1 deletion(-) (limited to 'lib') 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 -- cgit v1.3.1