From 1cb22cd29de924345cca651d0442b1fc56cf86db Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Mon, 16 Mar 2026 14:20:55 +0100 Subject: wip request/event (de-)marshalling --- lib/Wayland/Display.lean | 62 +++++++++++++++++++++++++++++++++++++++++++----- lib/Wayland/Native.lean | 6 ++--- 2 files changed, 59 insertions(+), 9 deletions(-) (limited to 'lib/Wayland') diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 2e2ceaa..4f356cb 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -25,7 +25,7 @@ def InterfaceName : Type := String /-- The numeric identifier of a request/event in an interface. -/ def OpCode : Type := UInt32 - deriving Repr, Nonempty, BEq, OfNat + deriving Repr, Nonempty, BEq, OfNat, DecidableEq /-- Handle to a client object, possibly dead. -/ structure Object (ι : InterfaceName) : Type where @@ -50,7 +50,7 @@ class ArgumentDemarshaller (m : Type → Type) extends Monad m where demarshalFixed : m Float32 demarshalString : m (Option String) demarshalObject {ι : InterfaceName} : m (Option (Object ι)) - demarshalNewID {ι : InterfaceName} : m (Object ι) + demarshalNewID : m UInt32 demarshalArray : m ByteArray demarshalFD : m Int32 @@ -121,6 +121,7 @@ structure Display (σ : Type) where private typeMap : Native.TypeMap private addTimer : (delayMs : UInt32) → (msg : Handler σ) → IO EventSource private addSignal : (signum : UInt32) → (msg : Handler σ) → IO EventSource + private listen : (proxy : Native.Proxy) → (handler : UInt32 → Native.ArgumentBuffer → Handler σ) → IO Unit private remove : (source : EventSource) → IO Unit private quit : IO Unit @@ -151,6 +152,7 @@ partial def DisplayM.run' (setUp : DisplayM σ Unit) (initialState : σ) (name : typeMap := typeMap addTimer := loop.addTimer addSignal := loop.addSignal + listen proxy handler := proxy.listen (fun x y ↦ ⟨loop, handler x y⟩) remove := loop.remove quit := loop.quit } let rec inner : StateT σ IO Unit := do @@ -221,14 +223,51 @@ def DisplayM.zoom {σ₁ σ₂ : Type} (lens : Lens σ₁ σ₂) (inner : Displa let global₂ : Display σ₂ := { disp := global₁.disp typeMap := global₁.typeMap - addTimer := fun x y ↦ global₁.addTimer x (zoomState lens y) - addSignal := fun x y ↦ global₁.addSignal x (zoomState lens y) + addTimer x y := global₁.addTimer x (zoomState lens y) + addSignal x y := global₁.addSignal x (zoomState lens y) + listen proxy handler := global₁.listen proxy (fun x y ↦ zoomState lens (handler x y)) remove := global₁.remove quit := global₁.quit } zoomState lens (ReaderT.run inner global₂) end DisplayMonad +section ArgumentMarshalling + +/-- Implementation of the `ArgumentReader` and `ArgumentWriter` monads using `Native.ArgumentBuffer`. -/ +private def ArgumentBufferM : Type → Type := + ReaderT Native.ArgumentBuffer IO + +deriving instance Monad for ArgumentBufferM + +private instance : MonadLift (ReaderT Native.ArgumentBuffer IO) ArgumentBufferM where + monadLift := id + +private instance : ArgumentMarshaller ArgumentBufferM where + marshalInt v := do (← read).writeInt v + marshalUInt v := do (← read).writeUInt v + marshalFixed v := do (← read).writeFixed v + marshalString v := do (← read).writeString v + marshalObject v := do (← read).writeObject (v.map Object.proxy) + marshalNewID v := do (← read).writeNewID v.proxy + marshalArray v := do (← read).writeArray v + marshalFD v := do (← read).writeFD v + +private instance : ArgumentDemarshaller ArgumentBufferM where + demarshalInt := do (← read).readInt + demarshalUInt := do (← read).readUInt + demarshalFixed := do (← read).readFixed + demarshalString := do (← read).readString + demarshalObject := do let proxy ← (← read).readObject; return proxy.map Object.mk + demarshalNewID := do (← read).readNewID + demarshalArray := do (← read).readArray + demarshalFD := do (← read).readFD + +private def ArgumentBufferM.run {α : Type} : ArgumentBufferM α → Native.ArgumentBuffer → IO α := + ReaderT.run + +end ArgumentMarshalling + section Proxies private def MessageDesc.toNative (msg : MessageDesc) : Native.Message := @@ -275,8 +314,19 @@ def DisplayM.createObject {ι ι' : InterfaceName} [iface : ResolvedInterface ι let proxy ← Native.Proxy.new factory.proxy typeMap ι return ⟨proxy⟩ --- 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 +/-- Send a request for an object to the server. -/ +def Object.send {ι : InterfaceName} [iface : Interface ι] (obj : Object ι) (req : iface.request) : DisplayM σ Unit := do + let argBuffer ← Native.ArgumentBuffer.new + let opcode ← ArgumentBufferM.run (iface.requestClass.marshal req) argBuffer + obj.proxy.send opcode argBuffer + +/-- Listen for events from the server for an object. -/ +def Object.listen {ι : InterfaceName} [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := do + let global ← read + let actualHandler (opcode : UInt32) (argBuffer : Native.ArgumentBuffer) : StateT σ IO Unit := do + let event ← ArgumentBufferM.run (iface.eventClass.demarshal opcode) argBuffer + ReaderT.run (handler event) global + global.listen obj.proxy actualHandler end Proxies diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index 9eb8398..0e8c079 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -86,7 +86,7 @@ opaque ArgumentBuffer.writeInt : (writer : @& ArgumentBuffer) → (value : Int32 opaque ArgumentBuffer.writeUInt : (writer : @& ArgumentBuffer) → (value : UInt32) → IO Unit @[extern "waylean_argument_buffer_write_fixed"] -opaque ArgumentBuffer.writeFloat : (writer : @& ArgumentBuffer) → (value : Float) → IO Unit +opaque ArgumentBuffer.writeFixed : (writer : @& ArgumentBuffer) → (value : Float32) → IO Unit @[extern "waylean_argument_buffer_write_string"] opaque ArgumentBuffer.writeString : (writer : @& ArgumentBuffer) → (value : @& Option String) → IO Unit @@ -107,10 +107,10 @@ opaque ArgumentBuffer.writeFD : (writer : @& ArgumentBuffer) → (value : Int32) opaque ArgumentBuffer.readInt : (reader : @& ArgumentBuffer) → IO Int32 @[extern "waylean_argument_buffer_read_uint"] -opaque ArgumentBuffer.readUInt : (reader : @& ArgumentBuffer) → IO Int32 +opaque ArgumentBuffer.readUInt : (reader : @& ArgumentBuffer) → IO UInt32 @[extern "waylean_argument_buffer_read_fixed"] -opaque ArgumentBuffer.readFixed : (reader : @& ArgumentBuffer) → IO Float +opaque ArgumentBuffer.readFixed : (reader : @& ArgumentBuffer) → IO Float32 @[extern "waylean_argument_buffer_read_string"] opaque ArgumentBuffer.readString : (reader : @& ArgumentBuffer) → IO (Option String) -- cgit v1.3.1