try to properly deal with constructors

4 files changed, 52 insertions, 108 deletions

diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc
index 7ff9332..abb9ee5 100644
--- a/lib/CWayland/CWayland.cc
+++ b/lib/CWayland/CWayland.cc
@@ -841,7 +841,7 @@ namespace
 {
     class argument_buffer
     {
-        enum class type { uninitialized, i32, u32, fixed, string, object, new_id, array, fd };
+        enum class type { uninitialized, i32, u32, fixed, string, object, array, fd };
         struct meta
         {
             type type{ type::uninitialized };
@@ -917,14 +917,6 @@ namespace
             meta[i].ref = std::move(value);
         }
 
-        void write_new_id(ref value)
-        {
-            auto i = next_write();
-            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)
         {
             auto i = next_write();
@@ -974,7 +966,7 @@ namespace
                     meta[i].ref = ref::steal(lean_box(0));
                 }
             }
-            else if (signature_type == "o" || signature_type == "?o")
+            else if (signature_type == "o" || signature_type == "?o" || signature_type == "n")
             {
                 meta[i].type = type::object;
                 if (arg.o)
@@ -990,10 +982,6 @@ namespace
                     meta[i].ref = ref::steal(lean_box(0));
                 }
             }
-            else if (signature_type == "n")
-            {
-                meta[i].type = type::new_id;
-            }
             else if (signature_type == "a")
             {
                 meta[i].type = type::array;
@@ -1041,12 +1029,6 @@ namespace
             return ref{ std::move(meta[i].ref) };
         }
 
-        ref read_new_id()
-        {
-            auto i = next_read(type::new_id);
-            return ref::steal(lean_box_uint32(args[i].n));
-        }
-
         ref read_array()
         {
             auto i = next_read(type::array);
@@ -1118,14 +1100,6 @@ lean_obj_res waylean_argument_buffer_write_object(b_lean_obj_arg buffer_obj, b_l
     return lean_io_result_mk_ok(lean_box(0));
 }
 
-// ArgumentBuffer.writeNewID : (buffer : @& ArgumentBuffer) → (value : @& Proxy) → IO Unit
-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));
-    buffer->write_new_id(ref{ value });
-    return lean_io_result_mk_ok(lean_box(0));
-}
-
 // ArgumentBuffer.writeArray : (buffer : @& ArgumentBuffer) → (value : @& ByteArray) → IO Unit
 lean_obj_res waylean_argument_buffer_write_array(b_lean_obj_arg buffer_obj, b_lean_obj_arg value)
 {
@@ -1177,13 +1151,6 @@ lean_obj_res waylean_argument_buffer_read_object(b_lean_obj_arg buffer_obj)
     return lean_io_result_mk_ok(buffer->read_object().release());
 }
 
-// ArgumentBuffer.readNewID : (buffer : @& ArgumentBuffer) → IO UInt32
-lean_obj_res waylean_argument_buffer_read_new_id(b_lean_obj_arg buffer_obj)
-{
-    auto buffer = static_cast<argument_buffer*>(lean_get_external_data(buffer_obj));
-    return lean_io_result_mk_ok(buffer->read_new_id().release());
-}
-
 // ArgumentBuffer.readArray : (buffer : @& ArgumentBuffer) → IO ByteArray
 lean_obj_res waylean_argument_buffer_read_array(b_lean_obj_arg buffer_obj)
 {
@@ -1204,7 +1171,6 @@ 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 };
@@ -1269,24 +1235,6 @@ lean_obj_res waylean_proxy_from_display(lean_obj_arg display)
     return lean_io_result_mk_ok(display);
 }
 
-// Proxy.new : (factory : @& Proxy) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy
-lean_obj_res waylean_proxy_new(b_lean_obj_arg factory_obj, b_lean_obj_arg map_obj, b_lean_obj_arg iface_name)
-{
-    auto factory = static_cast<wl_proxy*>(lean_get_external_data(factory_obj));
-    auto map = static_cast<type_map*>(lean_get_external_data(map_obj));
-    auto iface = map->resolve_iface(lean_string_cstr(iface_name));
-    
-    assert(iface->initialized && "expected interface to be initialized during construction");
-    wl_proxy* res = wl_proxy_create(factory, &iface->desc);
-    lean_object* waylean_res = lean_alloc_external(waylean_proxy_class(), res);
-    if (!res) { return io_result_mk_from_errno("<unknown>"); }
-    
-    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);
-}
-
 // Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → IO Unit
 lean_obj_res waylean_proxy_send(b_lean_obj_arg proxy_obj, uint32_t opcode, b_lean_obj_arg buffer_obj)
 {
@@ -1298,6 +1246,24 @@ lean_obj_res waylean_proxy_send(b_lean_obj_arg proxy_obj, uint32_t opcode, b_lea
     return lean_io_result_mk_ok(lean_box(0));
 }
 
+// Proxy.sendConstructor : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy
+lean_obj_res waylean_proxy_send_constructor(b_lean_obj_arg proxy_obj, uint32_t opcode, b_lean_obj_arg buffer_obj, b_lean_obj_arg map_obj, b_lean_obj_arg iface_name)
+{
+    auto proxy = static_cast<wl_proxy*>(lean_get_external_data(proxy_obj));
+    auto buffer = static_cast<argument_buffer*>(lean_get_external_data(buffer_obj));
+    auto map = static_cast<type_map*>(lean_get_external_data(map_obj));
+    auto iface = map->resolve_iface(lean_string_cstr(iface_name));
+    assert(iface->initialized && "expected interface to be initialized during construction");
+
+    wl_proxy* res = wl_proxy_marshal_array_constructor(proxy, opcode, buffer->get_args(), &iface->desc);
+    if (!res) { return io_result_mk_from_errno("<unknown>"); }
+
+    lean_object* waylean_res = lean_alloc_external(waylean_proxy_class(), res);
+    int stat = wl_proxy_add_dispatcher(res, dispatcher_func, waylean_res, nullptr);
+    
+    return lean_io_result_mk_ok(waylean_res);
+}
+
 // Proxy.listen : (proxy : @& Proxy) → (handler : UInt32 → ArgumentBuffer → EventLoop M × M) → IO Unit
 lean_obj_res waylean_proxy_listen(b_lean_obj_arg proxy_obj, lean_obj_arg handler)
 {
diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h
index eecc1eb..2db206e 100644
--- a/lib/CWayland/CWayland.h
+++ b/lib/CWayland/CWayland.h
@@ -54,8 +54,6 @@ lean_obj_res waylean_argument_buffer_write_string(b_lean_obj_arg writer,
                                                   b_lean_obj_arg value);
 lean_obj_res waylean_argument_buffer_write_object(b_lean_obj_arg writer,
                                                   b_lean_obj_arg value);
-lean_obj_res waylean_argument_buffer_write_new_id(b_lean_obj_arg writer,
-                                                  b_lean_obj_arg value);
 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,
@@ -65,21 +63,22 @@ 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
 
-lean_obj_res waylean_proxy_from_display(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_buffer);
-lean_obj_res waylean_proxy_listen      (b_lean_obj_arg proxy,
-                                        lean_obj_arg   handler);
+lean_obj_res waylean_proxy_from_display    (lean_obj_arg   display);
+lean_obj_res waylean_proxy_send            (b_lean_obj_arg proxy,
+                                            uint32_t       opcode,
+                                            b_lean_obj_arg argument_buffer);
+lean_obj_res waylean_proxy_send_constructor(b_lean_obj_arg proxy,
+                                            uint32_t       opcode,
+                                            b_lean_obj_arg argument_buffer,
+                                            b_lean_obj_arg type_map,
+                                            b_lean_obj_arg iface_name);
+lean_obj_res waylean_proxy_listen          (b_lean_obj_arg proxy,
+                                            lean_obj_arg   handler);
 
 #ifdef __cplusplus
 }
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 4f356cb..5747c4d 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -39,7 +39,6 @@ class ArgumentMarshaller (m : Type → Type) extends Monad m where
   marshalFixed                      : Float32           → m Unit
   marshalString                     : Option String     → m Unit
   marshalObject {ι : InterfaceName} : Option (Object ι) → m Unit
-  marshalNewID {ι : InterfaceName}  : Object ι          → m Unit
   marshalArray                      : ByteArray         → m Unit
   marshalFD                         : Int32             → m Unit
 
@@ -50,7 +49,6 @@ class ArgumentDemarshaller (m : Type → Type) extends Monad m where
   demarshalFixed                      : m Float32
   demarshalString                     : m (Option String)
   demarshalObject {ι : InterfaceName} : m (Option (Object ι))
-  demarshalNewID                      : m UInt32
   demarshalArray                      : m ByteArray
   demarshalFD                         : m Int32
 
@@ -77,24 +75,12 @@ structure MessageDesc where
   since : UInt32
   isDestructor : Bool
 
-/-- Class for types describing the request messages of an interface. -/
-class Request (α : Type) where
-  messages : Array MessageDesc
-  signature : α → MessageDesc
-  marshal {m : Type → Type} [ArgumentMarshaller m] : α → m OpCode
-
-/-- Class for types describing the event messages of an interface. -/
-class Event (α : Type) where
-  messages : Array MessageDesc
-  signature : α → MessageDesc
-  demarshal {m : Type → Type} [ArgumentDemarshaller m] : OpCode → m α
-
 /-- Class describing an interface. This is not associated with a type, but rather with the interface's name. -/
 class Interface (ι : InterfaceName) where
-  request : Type
-  [requestClass : Request request]
   event : Type
-  [eventClass : Event event]
+  requests : Array MessageDesc
+  events : Array MessageDesc
+  demarshalEvent {m : Type → Type} [ArgumentDemarshaller m] : OpCode → m event
   version : UInt32
 
 /-- Interface where all dependency interfaces can be resolvew. -/
@@ -249,7 +235,6 @@ private instance : ArgumentMarshaller ArgumentBufferM where
   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
 
@@ -259,7 +244,6 @@ private instance : ArgumentDemarshaller ArgumentBufferM where
   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
 
@@ -298,33 +282,34 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter
       typeMap.register
         { name := ι'
           version := iface'.version
-          requests := iface'.requestClass.messages.map MessageDesc.toNative
-          events := iface'.eventClass.messages.map MessageDesc.toNative }
+          requests := iface'.requests.map MessageDesc.toNative
+          events := iface'.events.map MessageDesc.toNative }
 
 /-- Get the `wl_display` instance within the display monad. -/
 def DisplayM.getDisplay : DisplayM σ (Object "wl_display") := do
   let proxy ← Native.Proxy.fromDisplay (← read).disp
   return ⟨proxy⟩
 
-/-- Create a new object, allocating a new ID in the client space and inheriting the display from the `factory`
-object. -/
-def DisplayM.createObject {ι ι' : InterfaceName} [iface : ResolvedInterface ι] (factory : Object ι') : DisplayM σ (Object ι) := do
-  ensureInterface ι
-  let typeMap := (← read).typeMap
-  let proxy ← Native.Proxy.new factory.proxy typeMap ι
-  return ⟨proxy⟩
-
-/-- Send a request for an object to the server. -/
-def Object.send {ι : InterfaceName} [iface : Interface ι] (obj : Object ι) (req : iface.request) : DisplayM σ Unit := do
+/-- Send a request for an object to the server that doesn't construct any new object. -/
+def Object.send {ι : InterfaceName} (obj : Object ι) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ Unit := do
   let argBuffer ← Native.ArgumentBuffer.new
-  let opcode ← ArgumentBufferM.run (iface.requestClass.marshal req) argBuffer
+  let opcode ← ArgumentBufferM.run marshaller argBuffer
   obj.proxy.send opcode argBuffer
 
+/-- Send a request for an object to the server, allocating a new id for a constructed object in the process. -/
+def Object.sendConstructor {ι ι' : InterfaceName} [iface : ResolvedInterface ι'] (obj : Object ι) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ (Object ι') := do
+  DisplayM.ensureInterface ι'
+  let typeMap := (← read).typeMap
+  let argBuffer ← Native.ArgumentBuffer.new
+  let opcode ← ArgumentBufferM.run marshaller argBuffer
+  let proxy ← obj.proxy.sendConstructor opcode argBuffer typeMap ι'
+  return ⟨proxy⟩
+
 /-- 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
+    let event ← ArgumentBufferM.run (iface.demarshalEvent opcode) argBuffer
     ReaderT.run (handler event) global
   global.listen obj.proxy actualHandler
 
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index 0e8c079..f8943ac 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -94,9 +94,6 @@ opaque ArgumentBuffer.writeString : (writer : @& ArgumentBuffer) → (value : @&
 @[extern "waylean_argument_buffer_write_object"]
 opaque ArgumentBuffer.writeObject : (writer : @& ArgumentBuffer) → (value : @& Option Proxy) → IO Unit
 
-@[extern "waylean_argument_buffer_write_new_id"]
-opaque ArgumentBuffer.writeNewID : (writer : @& ArgumentBuffer) → (value : @& Proxy) → IO Unit
-
 @[extern "waylean_argument_buffer_write_array"]
 opaque ArgumentBuffer.writeArray : (writer : @& ArgumentBuffer) → (value : @& ByteArray) → IO Unit
 
@@ -118,9 +115,6 @@ opaque ArgumentBuffer.readString : (reader : @& ArgumentBuffer) → IO (Option S
 @[extern "waylean_argument_buffer_read_object"]
 opaque ArgumentBuffer.readObject : (reader : @& ArgumentBuffer) → IO (Option Proxy)
 
-@[extern "waylean_argument_buffer_read_new_id"]
-opaque ArgumentBuffer.readNewID : (reader : @& ArgumentBuffer) → IO UInt32
-
 @[extern "waylean_argument_buffer_read_array"]
 opaque ArgumentBuffer.readArray : (reader : @& ArgumentBuffer) → IO ByteArray
 
@@ -130,12 +124,12 @@ opaque ArgumentBuffer.readFD : (reader : @& ArgumentBuffer) → IO Int32
 @[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) → (argumentBuffer : @& ArgumentBuffer) → IO Unit
 
+@[extern "waylean_proxy_send_constructor"]
+opaque Proxy.sendConstructor : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy
+
 @[extern "waylean_proxy_listen"]
 opaque Proxy.listen : (proxy : @& Proxy) → (handler : UInt32 → ArgumentBuffer → EventLoop M × M) → IO Unit