referenced interfaces

6 files changed, 52 insertions, 33 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
diff --git a/tools/Scanner/Processor.lean b/tools/Scanner/Processor.lean
index fad25bc..88853a6 100644
--- a/tools/Scanner/Processor.lean
+++ b/tools/Scanner/Processor.lean
@@ -11,9 +11,10 @@ private abbrev InterfaceMap := Std.TreeMap String InterfaceInfo
 
 private structure Context where
   interfaces : InterfaceMap
-  currentInterface : Identifier
+  currentInterface : Client.InterfaceRef
+  referencedInterfaces : Array Client.InterfaceRef
 
-private abbrev Processor : Type → Type := ReaderT Context (Except String)
+private abbrev Processor : Type → Type := StateT Context (Except String)
 
 private def processEnumEntry (raw : Raw.EnumEntryDesc) : Processor Client.EnumEntryDesc := do
   return {
@@ -25,21 +26,24 @@ private def processEnumEntry (raw : Raw.EnumEntryDesc) : Processor Client.EnumEn
   }
 
 private def interfaceInfo (name : String) : Processor InterfaceInfo := do
-  match (← read).interfaces.get? name with
+  match (← get).interfaces.get? name with
   | .some info => pure info
   | .none => .error s!"Unable to find referenced interface {name}"
 
 private def resolveInterface (name : String) : Processor Client.InterfaceRef := do
   let info ← interfaceInfo name
-  return {
+  let ref := {
     moduleName := info.moduleName
     typeName := name
   }
+  let old ← get
+  set { old with referencedInterfaces := old.referencedInterfaces ++ #[ref] }
+  return ref
 
 private def resolveEnum (name : String) : Processor Client.EnumRef := do
   let (interface, enum) ←
     match (name.split ".").toArray with
-    | #[enum]            => pure ((← read).currentInterface, enum.toString)
+    | #[enum]            => pure ((← get).currentInterface.typeName, enum.toString)
     | #[interface, enum] => pure (interface.toString, enum.toString)
     | _                  => throw s!"Malformed enum reference {name}"
   let info ← interfaceInfo interface
@@ -107,13 +111,21 @@ private def processEvent (raw : Raw.MessageDesc) : Processor Client.EventDesc :=
   }
 
 private def processInterface (raw : Raw.InterfaceDesc) : Processor Client.InterfaceDesc := do
+  let requests ← raw.requests.mapM processRequest
+  let events ← raw.events.mapM processEvent
+  let state ← get
+  let referencedInterfaces := state.referencedInterfaces ++ #[state.currentInterface]
   return {
     name := raw.name
     version := raw.version
     description := raw.description
     enums := ← raw.enums.mapM processEnum
-    requests := ← raw.requests.mapM processRequest
-    events := ← raw.events.mapM processEvent
+    requests := requests
+    events := events
+    referencedInterfaces := referencedInterfaces
+      |>.toList
+      |>.eraseDups
+      |>.toArray
   }
 
 private def processProtocol (interfaces : InterfaceMap) (raw : Raw.ProtocolDesc) : Except String Client.ProtocolDesc := do
@@ -122,9 +134,10 @@ private def processProtocol (interfaces : InterfaceMap) (raw : Raw.ProtocolDesc)
     copyright := raw.copyright
     description := raw.description
     interfaces := ← raw.interfaces.mapM
-      fun iface ↦ (processInterface iface).run {
+      fun iface ↦ (processInterface iface).run' {
         interfaces := interfaces
-        currentInterface := iface.name
+        currentInterface := { moduleName := raw.name, typeName := iface.name }
+        referencedInterfaces := #[]
       }
   }
 
diff --git a/tools/Scanner/Protocol.lean b/tools/Scanner/Protocol.lean
index 0ead630..c90ab56 100644
--- a/tools/Scanner/Protocol.lean
+++ b/tools/Scanner/Protocol.lean
@@ -164,6 +164,7 @@ structure InterfaceDesc where
   enums : Array EnumDesc
   requests : Array RequestDesc
   events : Array EventDesc
+  referencedInterfaces : Array InterfaceRef
   deriving Repr, BEq
 
 structure ProtocolDesc where