referenced interfaces

4 files changed, 29 insertions, 24 deletions

diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc
index cc9a9de..5f9b052 100644
--- a/lib/CWayland/CWayland.cc
+++ b/lib/CWayland/CWayland.cc
@@ -697,7 +697,8 @@ namespace
     struct interface
     {
         wl_interface desc;
-        bool initialized;
+        bool is_initialized;
+        bool is_complete;
     };
 
     class type_map
@@ -706,10 +707,10 @@ namespace
         std::unordered_map<std::string_view, interface*> interfaces;
 
     public:
-        bool contains_iface(std::string_view iface_name)
+        bool is_complete(std::string_view iface_name)
         {
             auto it = interfaces.find(iface_name);
-            return it != interfaces.end() && it->second->initialized;
+            return it != interfaces.end() && it->second->is_complete;
         }
 
         interface* resolve_iface(std::string_view iface_name)
@@ -721,13 +722,14 @@ namespace
             interface* iface = a.alloc_uninitialized<interface>();
             iface->desc = wl_interface{ 0 };
             iface->desc.name = name;
-            iface->initialized = false;
+            iface->is_initialized = false;
+            iface->is_complete= false;
 
             interfaces[name] = iface;
             return iface;
         }
 
-        void register_iface(b_lean_obj_arg iface_desc)
+        void register_iface(b_lean_obj_arg iface_desc, bool set_complete)
         {
             // structure Interface where
             //   name : String
@@ -738,8 +740,9 @@ namespace
             lean_object* iface_name = lean_ctor_get(iface_desc, 0);
 
             interface* iface = resolve_iface(lean_string_cstr(iface_name));
-            if (iface->initialized) { return; }
-            iface->initialized = true;
+            if (set_complete) { iface->is_complete = true; }
+            if (iface->is_initialized) { return; }
+            iface->is_initialized = true;
             wl_interface* desc = &iface->desc;
 
             lean_object* iface_requests = lean_ctor_get(iface_desc, 1);
@@ -817,19 +820,19 @@ lean_obj_res waylean_type_map_new(void)
     return lean_io_result_mk_ok(waylean_map);
 }
 
-// TypeMap.contains : (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Bool
-lean_obj_res waylean_type_map_contains(b_lean_obj_arg map_obj, b_lean_obj_arg iface_name)
+// TypeMap.isComplete : (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Bool
+lean_obj_res waylean_type_map_is_complete(b_lean_obj_arg map_obj, b_lean_obj_arg iface_name)
 {
     auto map = static_cast<type_map*>(lean_get_external_data(map_obj));
-    auto res = map->contains_iface(lean_string_cstr(iface_name));
+    auto res = map->is_complete(lean_string_cstr(iface_name));
     return lean_io_result_mk_ok(lean_box(res ? 1 : 0));
 }
 
-// TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → IO Unit
-lean_obj_res waylean_type_map_register(b_lean_obj_arg map_obj, b_lean_obj_arg iface_desc)
+// TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → (setComplete : UInt32) → IO Unit
+lean_obj_res waylean_type_map_register(b_lean_obj_arg map_obj, b_lean_obj_arg iface_desc, uint32_t set_complete)
 {
     auto map = static_cast<type_map*>(lean_get_external_data(map_obj));
-    map->register_iface(iface_desc);
+    map->register_iface(iface_desc, set_complete);
     return lean_io_result_mk_ok(lean_box(0));
 }
 
@@ -1250,7 +1253,7 @@ lean_obj_res waylean_proxy_send_constructor(b_lean_obj_arg proxy_obj, uint32_t o
     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");
+    assert(iface->is_complete && "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>"); }
diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h
index 1b8e0c8..74ed5e6 100644
--- a/lib/CWayland/CWayland.h
+++ b/lib/CWayland/CWayland.h
@@ -36,11 +36,12 @@ lean_obj_res waylean_event_loop_poll       (b_lean_obj_arg event_loop);
 
 // -- Type Map
 
-lean_obj_res waylean_type_map_new     (void);
-lean_obj_res waylean_type_map_contains(b_lean_obj_arg type_map,
-                                       b_lean_obj_arg iface_name);
-lean_obj_res waylean_type_map_register(b_lean_obj_arg type_map,
-                                       b_lean_obj_arg iface_desc);
+lean_obj_res waylean_type_map_new        (void);
+lean_obj_res waylean_type_map_is_complete(b_lean_obj_arg type_map,
+                                          b_lean_obj_arg iface_name);
+lean_obj_res waylean_type_map_register   (b_lean_obj_arg type_map,
+                                          b_lean_obj_arg iface_desc,
+                                          uint32_t       set_complete);
 
 // -- Argument Buffer
 
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 0a049b3..7bf55c5 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -281,13 +281,14 @@ private def MessageDesc.toNative (msg : MessageDesc) : Native.Message :=
 /-- 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
-    if !(← typeMap.contains ι') then
+  if not (← typeMap.isComplete ι) then
+    for ⟨ι', iface'⟩ in iface.referencedInterfaces do
       typeMap.register
         { name := ι'
           version := iface'.version
           requests := iface'.requests.map MessageDesc.toNative
           events := iface'.events.map MessageDesc.toNative }
+        (setComplete := if ι' == ι then 1 else 0)
 
 /-- Get the `wl_display` instance within the display monad. -/
 def DisplayM.getDisplay : DisplayM σ (Object "wl_display") := do
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index f8d4c53..430472b 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -73,11 +73,11 @@ opaque EventLoop.poll : (eventLoop : @& (EventLoop M)) → IO (Option M)
 @[extern "waylean_type_map_new"]
 opaque TypeMap.new : IO TypeMap
 
-@[extern "waylean_type_map_contains"]
-opaque TypeMap.contains : (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Bool
+@[extern "waylean_type_map_is_complete"]
+opaque TypeMap.isComplete : (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Bool
 
 @[extern "waylean_type_map_register"]
-opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → IO Unit
+opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → (setComplete : UInt32) → IO Unit
 
 @[extern "waylean_argument_buffer_new"]
 opaque ArgumentBuffer.new : IO ArgumentBuffer