outline proxy api

2 files changed, 25 insertions, 3 deletions

diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 76e5b7d..d42147c 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -28,7 +28,8 @@ def OpCode : Type := UInt32
   deriving Repr, Nonempty, BEq, OfNat
 
 /-- Handle to a client object, possibly dead. -/
-structure Object (ι : InterfaceName) where
+def Object (ι : InterfaceName) : Type := Native.Proxy
+  deriving Nonempty
 
 /-- Monad in which arguments can be marshalled one after another. -/
 class ArgumentMarshaller (m : Type → Type) extends Monad m where
@@ -95,7 +96,7 @@ class Interface (ι : InterfaceName) where
   [eventClass : Event event]
   version : UInt32
 
-/-- Interface where all dependent interfaces can be resolvew. -/
+/-- Interface where all dependency interfaces can be resolvew. -/
 class ResolvedInterface (ι : InterfaceName) where
   referencedInterfaces : Array ((ι' : InterfaceName) × Interface ι')
   contains_self : ∃ α, ⟨ι, α⟩ ∈ referencedInterfaces := by exists inferInstance; simp
@@ -249,6 +250,7 @@ private def MessageDesc.toNative (msg : MessageDesc) : Native.Message :=
     signature := s!"{msg.since}{String.join (msg.args.toList.map argString)}"
     types := msg.args.map argType }
 
+/-- 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
@@ -259,7 +261,6 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter
           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
 
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index e695e5f..f889c25 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -17,16 +17,25 @@ private opaque DisplayP : NonemptyType
 private opaque EventLoopP (M : Type) : NonemptyType
 private opaque EventSourceP : NonemptyType
 private opaque TypeMapP : NonemptyType
+private opaque ProxyP : NonemptyType
+private opaque ArgumentReaderP : NonemptyType
+private opaque ArgumentWriterP : NonemptyType
 
 def Display : Type := DisplayP.type
 def EventLoop (M : Type) : Type := (EventLoopP M).type
 def EventSource : Type := EventSourceP.type
 def TypeMap : Type := TypeMapP.type
+def Proxy : Type := ProxyP.type
+def ArgumentReader : Type := ArgumentReaderP.type
+def ArgumentWriter : Type := ArgumentWriterP.type
 
 instance : Nonempty Display := DisplayP.property
 instance : Nonempty (EventLoop M) := (EventLoopP M).property
 instance : Nonempty EventSource := EventSourceP.property
 instance : Nonempty TypeMap := TypeMapP.property
+instance : Nonempty Proxy := ProxyP.property
+instance : Nonempty ArgumentReader := ArgumentReaderP.property
+instance : Nonempty ArgumentWriter := ArgumentWriterP.property
 
 @[extern "waylean_SIGINT"]
 opaque SIGINT (u : Unit) : UInt32
@@ -73,4 +82,16 @@ opaque TypeMap.contains : (typeMap : @& TypeMap) → (ifaceName : @& String) →
 @[extern "waylean_type_map_register"]
 opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → IO Unit
 
+@[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) → (argumentWriter : @& ArgumentWriter) → IO Unit
+
+@[extern "waylean_proxy_listen"]
+opaque Proxy.listen : (proxy : @& Proxy) → (handler : @& (UInt32 → ArgumentReader → EventLoop M × M)) → IO Unit
+
 end Wayland.Native