From 0b7ad07db1be69f75ca9b469fd6210c64ba87dd5 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Fri, 13 Mar 2026 20:49:22 +0100 Subject: outline proxy api --- lib/Wayland/Display.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'lib/Wayland/Display.lean') diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 76e5b7d..d42147c 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -28,7 +28,8 @@ def OpCode : Type := UInt32 deriving Repr, Nonempty, BEq, OfNat /-- Handle to a client object, possibly dead. -/ -structure Object (ι : InterfaceName) where +def Object (ι : InterfaceName) : Type := Native.Proxy + deriving Nonempty /-- Monad in which arguments can be marshalled one after another. -/ class ArgumentMarshaller (m : Type → Type) extends Monad m where @@ -95,7 +96,7 @@ class Interface (ι : InterfaceName) where [eventClass : Event event] version : UInt32 -/-- Interface where all dependent interfaces can be resolvew. -/ +/-- Interface where all dependency interfaces can be resolvew. -/ class ResolvedInterface (ι : InterfaceName) where referencedInterfaces : Array ((ι' : InterfaceName) × Interface ι') contains_self : ∃ α, ⟨ι, α⟩ ∈ referencedInterfaces := by exists inferInstance; simp @@ -249,6 +250,7 @@ private def MessageDesc.toNative (msg : MessageDesc) : Native.Message := signature := s!"{msg.since}{String.join (msg.args.toList.map argString)}" types := msg.args.map argType } +/-- Ensure the given interface (and all of its dependencies) are registered in the display's `TypeMap`. -/ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInterface ι] : DisplayM σ Unit := do let typeMap := (← read).typeMap for ⟨ι', iface'⟩ in iface.referencedInterfaces do @@ -259,7 +261,6 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter requests := iface'.requestClass.messages.map MessageDesc.toNative events := iface'.eventClass.messages.map MessageDesc.toNative } - -- def Object.send [iface : Interface ι] (obj : Object ι) (req : iface.request) : DisplayM σ Unit := sorry -- def Object.listen [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := sorry -- cgit v1.3.1