type map implementation

6 files changed, 383 insertions, 98 deletions

diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc
index ecb87fc..57da46a 100644
--- a/lib/CWayland/CWayland.cc
+++ b/lib/CWayland/CWayland.cc
@@ -3,8 +3,10 @@
 #include <array>
 #include <vector>
 #include <queue>
+#include <memory>
 #include <unordered_map>
 #include <chrono>
+#include <cassert>
 #include <poll.h>
 #include <fcntl.h>
 #include <unistd.h>
@@ -623,6 +625,187 @@ lean_obj_res waylean_event_loop_quit(b_lean_obj_arg loop_obj)
 // EventLoop.poll : (eventLoop : @& EventLoop M) → IO (Option M)
 lean_obj_res waylean_event_loop_poll(b_lean_obj_arg loop_obj)
 {
+    struct wl_interface x; 
     auto loop = static_cast<event_loop*>(lean_get_external_data(loop_obj));
     return lean_io_result_mk_ok(loop->poll().release());
+}
+
+// -- Type Map
+
+namespace
+{
+    template<std::size_t Size = 4096>
+    class arena
+    {
+        struct region
+        {
+            std::array<std::byte, Size> buffer;
+            std::unique_ptr<region> prev;
+            std::size_t used{ 0 };
+        };
+
+        std::unique_ptr<region> curr;
+
+    public:
+        explicit arena()
+        {
+            curr = std::make_unique<region>();
+        }
+
+        template<typename T>
+        T* alloc_uninitialized(std::size_t count = 1)
+        {
+            std::size_t size = count * sizeof(T);
+            if (curr->used + size > Size)
+            {
+                // no more space -> allocate a new region
+                assert(size <= Size && "object too big for arena");
+                auto new_region = std::make_unique<region>();
+                new_region->prev = std::move(curr);
+                curr = std::move(new_region);
+            }
+
+            std::byte* res = &curr->buffer[curr->used];
+            curr->used += size;
+            return std::launder(reinterpret_cast<T*>(res));
+        }
+    };
+
+    struct interface
+    {
+        wl_interface desc;
+        bool initialized;
+    };
+
+    class type_map
+    {
+        arena<> a;
+        std::unordered_map<std::string_view, interface*> interfaces;
+
+    public:
+        bool contains_iface(std::string_view iface_name)
+        {
+            auto it = interfaces.find(iface_name);
+            return it != interfaces.end() && it->second->initialized;
+        }
+
+        interface* resolve_iface(std::string_view iface_name)
+        {
+            auto it = interfaces.find(iface_name);
+            if (it != interfaces.end()) { return it->second; }
+            
+            char* name = copy_string(iface_name);
+            interface* iface = a.alloc_uninitialized<interface>();
+            iface->desc = wl_interface{ 0 };
+            iface->desc.name = name;
+            iface->initialized = false;
+
+            interfaces[name] = iface;
+            return iface;
+        }
+
+        void register_iface(b_lean_obj_arg iface_desc)
+        {
+            // structure Interface where
+            //   name : String
+            //   version : UInt32
+            //   requests : Array Message
+            //   events : Array Message
+
+            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;
+            wl_interface* desc = &iface->desc;
+
+            lean_object* iface_requests = lean_ctor_get(iface_desc, 1);
+            std::size_t request_count = lean_array_size(iface_requests);
+            wl_message* requests = a.alloc_uninitialized<wl_message>(request_count);
+            for (std::size_t i = 0; i < request_count; ++i)
+            {
+                initialize_message(&requests[i], lean_array_get_core(iface_requests, i));
+            }
+            desc->method_count = request_count;
+            desc->methods = requests;
+
+            lean_object* iface_events = lean_ctor_get(iface_desc, 2);
+            std::size_t event_count = lean_array_size(iface_events);
+            wl_message* events = a.alloc_uninitialized<wl_message>(event_count);
+            for (std::size_t i = 0; i < event_count; ++i)
+            {
+                initialize_message(&events[i], lean_array_get_core(iface_events, i));
+            }
+            desc->event_count = event_count;
+            desc->events = events;
+
+            desc->version = lean_ctor_get_uint32(iface_desc, 3 * sizeof(void*));
+        }
+
+    private:
+        char* copy_string(std::string_view str)
+        {
+            char* res = a.alloc_uninitialized<char>(str.length() + 1);
+            std::copy(str.begin(), str.end(), res);
+            res[str.length()] = 0;
+            return res;
+        }
+
+        void initialize_message(wl_message* msg, b_lean_obj_arg msg_desc)
+        {
+            // structure Message where
+            //   name : String
+            //   signature : String
+            //   types : Array (Option String)
+
+            lean_object* msg_name = lean_ctor_get(msg_desc, 0);
+            msg->name = copy_string(lean_string_cstr(msg_name));
+
+            lean_object* msg_signature = lean_ctor_get(msg_desc, 1);
+            msg->signature = copy_string(lean_string_cstr(msg_signature));
+
+            lean_object* msg_types = lean_ctor_get(msg_desc, 2);
+            std::size_t type_count = lean_array_size(msg_types);
+            wl_interface const** types = a.alloc_uninitialized<wl_interface const*>(type_count);
+            for (std::size_t i = 0; i < type_count; ++i)
+            {
+                char const* type = option_cstr_or_null(lean_array_get_core(msg_types, i));
+                types[i] = type ? &resolve_iface(type)->desc : nullptr;
+            }
+            msg->types = types;
+        }
+    };
+
+    lean_external_class* waylean_type_map_class()
+    {
+        static lean_external_class* klass = lean_register_external_class(
+            [](void* ptr) { delete static_cast<type_map*>(ptr); },
+            [](void*, b_lean_obj_arg fn) { }
+        );
+        return klass;
+    }
+}
+
+// TypeMap.new : IO TypeMap
+lean_obj_res waylean_type_map_new(void)
+{
+    type_map* map = new type_map;
+    lean_object* waylean_map = lean_alloc_external(waylean_type_map_class(), map);
+    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)
+{
+    auto map = static_cast<type_map*>(lean_get_external_data(map_obj));
+    auto res = map->contains_iface(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)
+{
+    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));
 }
\ No newline at end of file
diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h
index 75d2e0d..6c8e002 100644
--- a/lib/CWayland/CWayland.h
+++ b/lib/CWayland/CWayland.h
@@ -34,6 +34,20 @@ lean_obj_res waylean_event_loop_remove     (b_lean_obj_arg event_loop,
 lean_obj_res waylean_event_loop_quit       (b_lean_obj_arg event_loop);
 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);
+
+// -- Proxy
+
+// -- Argument Marshaller
+
+// -- Argument Demarshaller
+
 #ifdef __cplusplus
 }
 #endif
\ No newline at end of file
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 7c628f3..76e5b7d 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -16,9 +16,99 @@ variable {σ α : Type}
 
 namespace Wayland
 
+section Interfaces
+
+/-- The name of an interface (e.g., `"wl_display"`), commonly used to resolve the corresponding interface description
+using the `Interface` class. -/
+def InterfaceName : Type := String
+  deriving Repr, Nonempty, BEq, ToString
+
+/-- The numeric identifier of a request/event in an interface. -/
+def OpCode : Type := UInt32
+  deriving Repr, Nonempty, BEq, OfNat
+
+/-- Handle to a client object, possibly dead. -/
+structure Object (ι : InterfaceName) where
+
+/-- Monad in which arguments can be marshalled one after another. -/
+class ArgumentMarshaller (m : Type → Type) extends Monad m where
+  marshalInt                        : Int32             → m Unit
+  marshalUInt                       : UInt32            → m Unit
+  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
+
+/-- Monad in which arguments can be demarshalled one after another. -/
+class ArgumentDemarshaller (m : Type → Type) extends Monad m where
+  demarshalInt                        : m Int32
+  demarshalUInt                       : m UInt32
+  demarshalFixed                      : m Float32
+  demarshalString                     : m (Option String)
+  demarshalObject {ι : InterfaceName} : m (Option (Object ι))
+  demarshalNewID {ι : InterfaceName}  : m (Object ι)
+  demarshalArray                      : m ByteArray
+  demarshalFD                         : m Int32
+
+/-- Nullability annotation in an interface's message. -/
+inductive Nullability where
+  | nullable
+  | notNull
+
+/-- Argument description in an interface's message. -/
+inductive ArgumentDesc where
+  | int : ArgumentDesc
+  | uint : ArgumentDesc
+  | fixed : ArgumentDesc
+  | string : Nullability → ArgumentDesc
+  | object : Nullability → InterfaceName → ArgumentDesc
+  | newID : InterfaceName → ArgumentDesc
+  | array : ArgumentDesc
+  | fd : ArgumentDesc
+
+/-- Message description for an interface. -/
+structure MessageDesc where
+  name : String
+  args : Array ArgumentDesc
+  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]
+  version : UInt32
+
+/-- Interface where all dependent interfaces can be resolvew. -/
+class ResolvedInterface (ι : InterfaceName) where
+  referencedInterfaces : Array ((ι' : InterfaceName) × Interface ι')
+  contains_self : ∃ α, ⟨ι, α⟩ ∈ referencedInterfaces := by exists inferInstance; simp
+  -- TODO: Verify that dependencies of interfaces are in referencedInterfaces
+
+end Interfaces
+
+section DisplayMonad
+
 /-- A token managing a single source of events such as a timer or a signal handler. This can be used to unregister the
 event. -/
 def EventSource : Type := Native.EventSource
+  deriving Nonempty
 
 /-- Internal handler interface passed as a message to the event loop. -/
 private abbrev Handler (σ : Type) := StateT σ IO Unit
@@ -26,6 +116,7 @@ private abbrev Handler (σ : Type) := StateT σ IO Unit
 /-- Access to the display and event loop, providing the main functionality. -/
 structure Display (σ : Type) where
   private disp : Native.Display
+  private typeMap : Native.TypeMap
   private addTimer : (delayMs : UInt32) → (msg : Handler σ) → IO EventSource
   private addSignal : (signum : UInt32) → (msg : Handler σ) → IO EventSource
   private remove : (source : EventSource) → IO Unit
@@ -50,10 +141,12 @@ Parameters:
 · `name`: Socket name for connecting to the Wayland server (by default, `wayland-0` is used). -/
 partial def DisplayM.run' (setUp : DisplayM σ Unit) (initialState : σ) (name : Option String := .none) : IO σ := do
   let disp ← Native.Display.new name
+  let typeMap ← Native.TypeMap.new
   let loop ← Native.EventLoop.new
   _ ← loop.addDisplay disp
   let global : Display σ :=
     { disp := disp
+      typeMap := typeMap
       addTimer := loop.addTimer
       addSignal := loop.addSignal
       remove := loop.remove
@@ -125,10 +218,51 @@ def DisplayM.zoom {σ₁ σ₂ : Type} (lens : Lens σ₁ σ₂) (inner : Displa
   let global₁ : Display σ₁ ← read
   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)
       remove := global₁.remove
       quit := global₁.quit }
   zoomState lens (ReaderT.run inner global₂)
 
+end DisplayMonad
+
+section Proxies
+
+private def MessageDesc.toNative (msg : MessageDesc) : Native.Message :=
+  let argString : ArgumentDesc → String
+    | .int => "i"
+    | .uint => "u"
+    | .fixed => "f"
+    | .string .nullable => "?s"
+    | .string .notNull => "s"
+    | .object .nullable _ => "?o"
+    | .object .notNull _ => "o"
+    | .newID _ => "n"
+    | .array => "a"
+    | .fd => "h"
+  let argType : ArgumentDesc → Option String
+    | .object _ iface => .some iface
+    | .newID iface => .some iface
+    | _ => .none
+  { name := msg.name
+    signature := s!"{msg.since}{String.join (msg.args.toList.map argString)}"
+    types := msg.args.map argType }
+
+private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInterface ι] : DisplayM σ Unit := do
+  let typeMap := (← read).typeMap
+  for ⟨ι', iface'⟩ in iface.referencedInterfaces do
+    if !(← typeMap.contains ι') then
+      typeMap.register
+        { name := ι'
+          version := iface'.version
+          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
+
+end Proxies
+
 end Wayland
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index bd85291..e695e5f 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -2,17 +2,31 @@ variable {M : Type}
 
 namespace Wayland.Native
 
+structure Message where
+  name : String
+  signature : String
+  types : Array (Option String)
+
+structure Interface where
+  name : String
+  version : UInt32
+  requests : Array Message
+  events : Array Message
+
 private opaque DisplayP : NonemptyType
 private opaque EventLoopP (M : Type) : NonemptyType
 private opaque EventSourceP : NonemptyType
+private opaque TypeMapP : NonemptyType
 
 def Display : Type := DisplayP.type
 def EventLoop (M : Type) : Type := (EventLoopP M).type
 def EventSource : Type := EventSourceP.type
+def TypeMap : Type := TypeMapP.type
 
 instance : Nonempty Display := DisplayP.property
 instance : Nonempty (EventLoop M) := (EventLoopP M).property
 instance : Nonempty EventSource := EventSourceP.property
+instance : Nonempty TypeMap := TypeMapP.property
 
 @[extern "waylean_SIGINT"]
 opaque SIGINT (u : Unit) : UInt32
@@ -50,4 +64,13 @@ opaque EventLoop.quit : (eventLoop : @& (EventLoop M)) → IO Unit
 @[extern "waylean_event_loop_poll"]
 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_register"]
+opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → IO Unit
+
 end Wayland.Native
diff --git a/lib/Wayland/Object.lean b/lib/Wayland/Object.lean
deleted file mode 100644
index 6c5dbb7..0000000
--- a/lib/Wayland/Object.lean
+++ /dev/null
@@ -1,98 +0,0 @@
-import Wayland.Display
-
-namespace Wayland
-
-def InterfaceName : Type := String
-  deriving Repr, BEq
-
-def OpCode : Type := UInt32
-  deriving Repr, BEq
-
-structure Object (ι : InterfaceName) where
-
-structure NewID (ι : InterfaceName) where
-
-class ArgumentMarshaller (m : Type → Type) extends Monad m where
-  marshalInt                        : Int32             → m Unit
-  marshalUInt                       : UInt32            → m Unit
-  marshalFixed                      : Float32           → m Unit
-  marshalString                     : Option String     → m Unit
-  marshalObject {ι : InterfaceName} : Option (Object ι) → m Unit
-  marshalNewID {ι : InterfaceName}  : NewID ι           → m Unit
-  marshalArray                      : ByteArray         → m Unit
-  marshalFD                         : Int32             → m Unit
-
-class ArgumentDemarshaller (m : Type → Type) extends Monad m where
-  demarshalInt                        : m Int32
-  demarshalUInt                       : m UInt32
-  demarshalFixed                      : m Float32
-  demarshalString                     : m (Option String)
-  demarshalObject {ι : InterfaceName} : m (Option (Object ι))
-  demarshalNewID {ι : InterfaceName}  : m (NewID ι)
-  demarshalArray                      : m ByteArray
-  demarshalFD                         : m Int32
-
-inductive Nullability where
-  | nullable
-  | notNull
-
-inductive Argument where
-  | int : Argument
-  | uint : Argument
-  | fixed : Argument
-  | string : Nullability → Argument
-  | object : Nullability → InterfaceName → Argument
-  | newID : InterfaceName → Argument
-  | array : Argument
-  | fd : Argument
-
-structure Message where
-  name : String
-  args : Array Argument
-  since : UInt32
-  isDestructor : Bool
-
-class Request (α : Type) where
-  messages : Array Message
-  signature : α → Message
-  marshal {m : Type → Type} [ArgumentMarshaller m] : α → m OpCode
-
-class Event (α : Type) where
-  messages : Array Message
-  signature : α → Message
-  demarshal {m : Type → Type} [ArgumentDemarshaller m] : OpCode → m α
-
-class Interface (ι : InterfaceName) where
-  request : Type
-  [requestClass : Request request]
-  event : Type
-  [eventClass : Event event]
-  version : UInt32
-
-variable {σ : Type} {ι : InterfaceName}
-
-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
-
--- def WLDisplay.name : InterfaceName := "wl_display"
--- abbrev WLDisplay : Type := Object WLDisplay.name
-
--- inductive WLDisplay.Request where
---   | sync : Request
-
--- inductive WLDisplay.Event where
---   | error : Event
-
--- instance : Request WLDisplay.Request := sorry
--- instance : Event WLDisplay.Event := sorry
--- instance : Interface WLDisplay.name where
---   request := WLDisplay.Request
---   event := WLDisplay.Event
---   version := 1
-
--- def test (disp : WLDisplay) : DisplayM σ Unit := do
---   disp.listen fun
---     | .error => DisplayM.liftIO (IO.println "error!")
---   disp.send .sync
-
-end Wayland
diff --git a/src/Waylean.lean b/src/Waylean.lean
index 354b609..3565854 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -1,6 +1,35 @@
 import Wayland
 open Wayland
 
+
+def WLDisplay.name : InterfaceName := "wl_display"
+abbrev WLDisplay : Type := Object WLDisplay.name
+
+inductive WLDisplay.Request where
+  | sync : Request
+
+inductive WLDisplay.Event where
+  | error : Event
+  | other : Event
+
+instance : Request WLDisplay.Request where
+  messages := #[{ name := "sync", args := #[], since := 0, isDestructor := False }]
+  signature _ := sorry
+  marshal _ := do return 0
+instance : Event WLDisplay.Event where
+  messages := #[{ name := "error", args := #[.string .notNull], since := 0, isDestructor := False },
+                { name := "other", args := #[.object .nullable WLDisplay.name], since := 99, isDestructor := False}]
+  signature _ := sorry
+  demarshal _ := do return .error
+instance : Interface WLDisplay.name where
+  request := WLDisplay.Request
+  event := WLDisplay.Event
+  version := 1
+instance : ResolvedInterface WLDisplay.name where
+  referencedInterfaces := #[⟨WLDisplay.name, inferInstance⟩]
+
+
+
 structure State where
   count : Int