wip request/event (de-)marshalling

4 files changed, 81 insertions, 26 deletions

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 : "<default>"); }
     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<wl_object*>(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<argument_buffer*>(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<argument_buffer*>(lean_get_external_data(buffer_obj));
-    auto proxy = static_cast<wl_proxy*>(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<argument_buffer*>(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("<unknown>"); }
     
-    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<wl_proxy*>(lean_get_external_data(proxy_obj));
     auto buffer = static_cast<argument_buffer*>(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)