diff options
| -rw-r--r-- | lib/CWayland/CWayland.cc | 22 | ||||
| -rw-r--r-- | lib/CWayland/CWayland.h | 44 | ||||
| -rw-r--r-- | lib/Wayland/Display.lean | 7 | ||||
| -rw-r--r-- | lib/Wayland/Native.lean | 21 |
4 files changed, 87 insertions, 7 deletions
diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc index 57da46a..cf1687a 100644 --- a/lib/CWayland/CWayland.cc +++ b/lib/CWayland/CWayland.cc @@ -808,4 +808,26 @@ lean_obj_res waylean_type_map_register(b_lean_obj_arg map_obj, b_lean_obj_arg if auto map = static_cast<type_map*>(lean_get_external_data(map_obj)); map->register_iface(iface_desc); return lean_io_result_mk_ok(lean_box(0)); +} + +// -- Proxy + +// Proxy.fromDisplay : (display : @& Display) → IO Proxy +lean_obj_res waylean_proxy_from_display(b_lean_obj_arg display) +{ +} + +// Proxy.new : (factory : @& Proxy) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy +lean_obj_res waylean_proxy_new(b_lean_obj_arg factory, b_lean_obj_arg type_map, b_lean_obj_arg iface_name) +{ +} + +// Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentWriter : @& ArgumentWriter) → IO Unit +lean_obj_res waylean_proxy_send(b_lean_obj_arg proxy, uint32_t opcode, b_lean_obj_arg argument_writer) +{ +} + +// Proxy.listen : (proxy : @& Proxy) → (handler : @& UInt32 → ArgumentReader → EventLoop M × M) → IO Unit +lean_obj_res waylean_proxy_listen(b_lean_obj_arg proxy, b_lean_obj_arg handler) +{ }
\ No newline at end of file diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h index 6c8e002..e0bcfa2 100644 --- a/lib/CWayland/CWayland.h +++ b/lib/CWayland/CWayland.h @@ -15,8 +15,7 @@ uint32_t waylean_SIGUSR2(void); // -- Display -lean_obj_res waylean_display_new (b_lean_obj_arg name); -lean_obj_res waylean_display_roundtrip(b_lean_obj_arg display); +lean_obj_res waylean_display_new(b_lean_obj_arg name); // -- Event Loop @@ -44,9 +43,46 @@ lean_obj_res waylean_type_map_register(b_lean_obj_arg type_map, // -- Proxy -// -- Argument Marshaller +lean_obj_res waylean_proxy_from_display(b_lean_obj_arg display); +lean_obj_res waylean_proxy_new (b_lean_obj_arg factory, + b_lean_obj_arg type_map, + b_lean_obj_arg iface_name); +lean_obj_res waylean_proxy_send (b_lean_obj_arg proxy, + uint32_t opcode, + b_lean_obj_arg argument_writer); +lean_obj_res waylean_proxy_listen (b_lean_obj_arg proxy, + b_lean_obj_arg handler); -// -- Argument Demarshaller +// -- Argument Writer + +lean_obj_res waylean_argument_writer_new (void); +lean_obj_res waylean_argument_writer_write_int (b_lean_obj_arg writer, + int32_t value); +lean_obj_res waylean_argument_writer_write_uint (b_lean_obj_arg writer, + uint32_t value); +lean_obj_res waylean_argument_writer_write_fixed (b_lean_obj_arg writer, + float value); +lean_obj_res waylean_argument_writer_write_string(b_lean_obj_arg writer, + b_lean_obj_arg value); +lean_obj_res waylean_argument_writer_write_object(b_lean_obj_arg writer, + b_lean_obj_arg value); +lean_obj_res waylean_argument_writer_write_new_id(b_lean_obj_arg writer, + b_lean_obj_arg value); +lean_obj_res waylean_argument_writer_write_array (b_lean_obj_arg writer, + b_lean_obj_arg value); +lean_obj_res waylean_argument_writer_write_fd (b_lean_obj_arg writer, + int32_t value); + +// -- Argument Reader + +lean_obj_res waylean_argument_reader_read_int (b_lean_obj_arg reader); +lean_obj_res waylean_argument_reader_read_uint (b_lean_obj_arg reader); +lean_obj_res waylean_argument_reader_read_fixed (b_lean_obj_arg reader); +lean_obj_res waylean_argument_reader_read_string(b_lean_obj_arg reader); +lean_obj_res waylean_argument_reader_read_object(b_lean_obj_arg reader); +lean_obj_res waylean_argument_reader_read_new_id(b_lean_obj_arg reader); +lean_obj_res waylean_argument_reader_read_array (b_lean_obj_arg reader); +lean_obj_res waylean_argument_reader_read_fd (b_lean_obj_arg reader); #ifdef __cplusplus } 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 diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index e695e5f..f889c25 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -17,16 +17,25 @@ private opaque DisplayP : NonemptyType private opaque EventLoopP (M : Type) : NonemptyType private opaque EventSourceP : NonemptyType private opaque TypeMapP : NonemptyType +private opaque ProxyP : NonemptyType +private opaque ArgumentReaderP : NonemptyType +private opaque ArgumentWriterP : NonemptyType def Display : Type := DisplayP.type def EventLoop (M : Type) : Type := (EventLoopP M).type def EventSource : Type := EventSourceP.type def TypeMap : Type := TypeMapP.type +def Proxy : Type := ProxyP.type +def ArgumentReader : Type := ArgumentReaderP.type +def ArgumentWriter : Type := ArgumentWriterP.type instance : Nonempty Display := DisplayP.property instance : Nonempty (EventLoop M) := (EventLoopP M).property instance : Nonempty EventSource := EventSourceP.property instance : Nonempty TypeMap := TypeMapP.property +instance : Nonempty Proxy := ProxyP.property +instance : Nonempty ArgumentReader := ArgumentReaderP.property +instance : Nonempty ArgumentWriter := ArgumentWriterP.property @[extern "waylean_SIGINT"] opaque SIGINT (u : Unit) : UInt32 @@ -73,4 +82,16 @@ opaque TypeMap.contains : (typeMap : @& TypeMap) → (ifaceName : @& String) → @[extern "waylean_type_map_register"] opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → IO Unit +@[extern "waylean_proxy_from_display"] +opaque Proxy.fromDisplay : (display : @& Display) → IO Proxy + +@[extern "waylean_proxy_new"] +opaque Proxy.new : (factory : @& Proxy) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy + +@[extern "waylean_proxy_send"] +opaque Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentWriter : @& ArgumentWriter) → IO Unit + +@[extern "waylean_proxy_listen"] +opaque Proxy.listen : (proxy : @& Proxy) → (handler : @& (UInt32 → ArgumentReader → EventLoop M × M)) → IO Unit + end Wayland.Native |