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/CWayland/CWayland.cc | 23 +++++++++++------- lib/CWayland/CWayland.h | 16 ++++++------- lib/Wayland/Display.lean | 62 +++++++++++++++++++++++++++++++++++++++++++----- lib/Wayland/Native.lean | 6 ++--- 4 files changed, 81 insertions(+), 26 deletions(-) (limited to 'lib') diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc index 718785f..7ff9332 100644 --- a/lib/CWayland/CWayland.cc +++ b/lib/CWayland/CWayland.cc @@ -174,7 +174,7 @@ lean_obj_res waylean_display_new(b_lean_obj_arg name) if (!disp) { return io_result_mk_from_errno(name_cstr ? name_cstr : ""); } lean_object* waylean_disp = lean_alloc_external(waylean_display_class(), disp); - wl_proxy_add_dispatcher((wl_proxy*)disp, dispatcher_func, waylean_disp, nullptr); + // wl_proxy_add_dispatcher((wl_proxy*)disp, dispatcher_func, waylean_disp, nullptr); return lean_io_result_mk_ok(waylean_disp); } @@ -870,6 +870,7 @@ namespace } public: + int get_count() { return writer_idx; } wl_argument* get_args() { return args.data(); } void write_int(int32_t value) @@ -916,11 +917,12 @@ namespace meta[i].ref = std::move(value); } - void write_new_id(std::uint32_t value) + void write_new_id(ref value) { auto i = next_write(); - args[i].n = value; - meta[i].type = type::new_id; + args[i].o = static_cast(lean_get_external_data(value.get())); + meta[i].type = type::object; + meta[i].ref = std::move(value); } void write_array(ref value) @@ -1092,7 +1094,7 @@ lean_obj_res waylean_argument_buffer_write_uint(b_lean_obj_arg buffer_obj, uint3 return lean_io_result_mk_ok(lean_box(0)); } -// ArgumentBuffer.writeFloat : (buffer : @& ArgumentBuffer) → (value : Float) → IO Unit +// ArgumentBuffer.writeFixed : (buffer : @& ArgumentBuffer) → (value : Float) → IO Unit lean_obj_res waylean_argument_buffer_write_fixed(b_lean_obj_arg buffer_obj, float value) { auto buffer = static_cast(lean_get_external_data(buffer_obj)); @@ -1120,8 +1122,7 @@ lean_obj_res waylean_argument_buffer_write_object(b_lean_obj_arg buffer_obj, b_l lean_obj_res waylean_argument_buffer_write_new_id(b_lean_obj_arg buffer_obj, b_lean_obj_arg value) { auto buffer = static_cast(lean_get_external_data(buffer_obj)); - auto proxy = static_cast(lean_get_external_data(value)); - buffer->write_new_id(wl_proxy_get_id(proxy)); + buffer->write_new_id(ref{ value }); return lean_io_result_mk_ok(lean_box(0)); } @@ -1148,7 +1149,7 @@ lean_obj_res waylean_argument_buffer_read_int(b_lean_obj_arg buffer_obj) return lean_io_result_mk_ok(buffer->read_int().release()); } -// ArgumentBuffer.readUInt : (buffer : @& ArgumentBuffer) → IO Int32 +// ArgumentBuffer.readUInt : (buffer : @& ArgumentBuffer) → IO UInt32 lean_obj_res waylean_argument_buffer_read_uint(b_lean_obj_arg buffer_obj) { auto buffer = static_cast(lean_get_external_data(buffer_obj)); @@ -1203,6 +1204,7 @@ namespace { int dispatcher_func(const void* user_data, void* target, uint32_t opcode, const wl_message* msg, wl_argument* args) { + fprintf(stderr, "Dispatcher func!\n"); if (!user_data) { return 0; } auto handler = ref{ (lean_object*)user_data }; @@ -1279,7 +1281,8 @@ lean_obj_res waylean_proxy_new(b_lean_obj_arg factory_obj, b_lean_obj_arg map_ob lean_object* waylean_res = lean_alloc_external(waylean_proxy_class(), res); if (!res) { return io_result_mk_from_errno(""); } - wl_proxy_add_dispatcher(res, dispatcher_func, waylean_res, nullptr); + int stat = wl_proxy_add_dispatcher(res, dispatcher_func, waylean_res, nullptr); + fprintf(stderr, "add_dispatcher: %d\n", stat); return lean_io_result_mk_ok(waylean_res); } @@ -1289,7 +1292,9 @@ lean_obj_res waylean_proxy_send(b_lean_obj_arg proxy_obj, uint32_t opcode, b_lea { auto proxy = static_cast(lean_get_external_data(proxy_obj)); auto buffer = static_cast(lean_get_external_data(buffer_obj)); + wl_proxy_marshal_array(proxy, opcode, buffer->get_args()); + return lean_io_result_mk_ok(lean_box(0)); } diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h index fbfea9b..eecc1eb 100644 --- a/lib/CWayland/CWayland.h +++ b/lib/CWayland/CWayland.h @@ -60,14 +60,14 @@ lean_obj_res waylean_argument_buffer_write_array (b_lean_obj_arg writer, b_lean_obj_arg value); lean_obj_res waylean_argument_buffer_write_fd (b_lean_obj_arg writer, int32_t value); -lean_obj_res waylean_argument_buffer_read_int (b_lean_obj_arg reader); -lean_obj_res waylean_argument_buffer_read_uint (b_lean_obj_arg reader); -lean_obj_res waylean_argument_buffer_read_fixed (b_lean_obj_arg reader); -lean_obj_res waylean_argument_buffer_read_string(b_lean_obj_arg reader); -lean_obj_res waylean_argument_buffer_read_object(b_lean_obj_arg reader); -lean_obj_res waylean_argument_buffer_read_new_id(b_lean_obj_arg reader); -lean_obj_res waylean_argument_buffer_read_array (b_lean_obj_arg reader); -lean_obj_res waylean_argument_buffer_read_fd (b_lean_obj_arg reader); +lean_obj_res waylean_argument_buffer_read_int (b_lean_obj_arg reader); +lean_obj_res waylean_argument_buffer_read_uint (b_lean_obj_arg reader); +lean_obj_res waylean_argument_buffer_read_fixed (b_lean_obj_arg reader); +lean_obj_res waylean_argument_buffer_read_string (b_lean_obj_arg reader); +lean_obj_res waylean_argument_buffer_read_object (b_lean_obj_arg reader); +lean_obj_res waylean_argument_buffer_read_new_id (b_lean_obj_arg reader); +lean_obj_res waylean_argument_buffer_read_array (b_lean_obj_arg reader); +lean_obj_res waylean_argument_buffer_read_fd (b_lean_obj_arg reader); // -- Proxy 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