1 files changed, 18 insertions, 33 deletions

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