wip request/event (de-)marshalling

2 files changed, 59 insertions, 9 deletions

diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 2e2ceaa..4f356cb 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -25,7 +25,7 @@ def InterfaceName : Type := String
 
 /-- The numeric identifier of a request/event in an interface. -/
 def OpCode : Type := UInt32
-  deriving Repr, Nonempty, BEq, OfNat
+  deriving Repr, Nonempty, BEq, OfNat, DecidableEq
 
 /-- Handle to a client object, possibly dead. -/
 structure Object (ι : InterfaceName) : Type where
@@ -50,7 +50,7 @@ class ArgumentDemarshaller (m : Type → Type) extends Monad m where
   demarshalFixed                      : m Float32
   demarshalString                     : m (Option String)
   demarshalObject {ι : InterfaceName} : m (Option (Object ι))
-  demarshalNewID {ι : InterfaceName}  : m (Object ι)
+  demarshalNewID                      : m UInt32
   demarshalArray                      : m ByteArray
   demarshalFD                         : m Int32
 
@@ -121,6 +121,7 @@ structure Display (σ : Type) where
   private typeMap : Native.TypeMap
   private addTimer : (delayMs : UInt32) → (msg : Handler σ) → IO EventSource
   private addSignal : (signum : UInt32) → (msg : Handler σ) → IO EventSource
+  private listen : (proxy : Native.Proxy) → (handler : UInt32 → Native.ArgumentBuffer → Handler σ) → IO Unit
   private remove : (source : EventSource) → IO Unit
   private quit : IO Unit
 
@@ -151,6 +152,7 @@ partial def DisplayM.run' (setUp : DisplayM σ Unit) (initialState : σ) (name :
       typeMap := typeMap
       addTimer := loop.addTimer
       addSignal := loop.addSignal
+      listen proxy handler := proxy.listen (fun x y ↦ ⟨loop, handler x y⟩)
       remove := loop.remove
       quit := loop.quit }
   let rec inner : StateT σ IO Unit := do
@@ -221,14 +223,51 @@ def DisplayM.zoom {σ₁ σ₂ : Type} (lens : Lens σ₁ σ₂) (inner : Displa
   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)
+      addTimer x y := global₁.addTimer x (zoomState lens y)
+      addSignal x y := global₁.addSignal x (zoomState lens y)
+      listen proxy handler := global₁.listen proxy (fun x y ↦ zoomState lens (handler x y))
       remove := global₁.remove
       quit := global₁.quit }
   zoomState lens (ReaderT.run inner global₂)
 
 end DisplayMonad
 
+section ArgumentMarshalling
+
+/-- Implementation of the `ArgumentReader` and `ArgumentWriter` monads using `Native.ArgumentBuffer`. -/
+private def ArgumentBufferM : Type → Type :=
+  ReaderT Native.ArgumentBuffer IO
+
+deriving instance Monad for ArgumentBufferM
+
+private instance : MonadLift (ReaderT Native.ArgumentBuffer IO) ArgumentBufferM where
+  monadLift := id
+
+private instance : ArgumentMarshaller ArgumentBufferM where
+  marshalInt v := do (← read).writeInt v
+  marshalUInt v := do (← read).writeUInt v
+  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
+
+private instance : ArgumentDemarshaller ArgumentBufferM where
+  demarshalInt := do (← read).readInt
+  demarshalUInt := do (← read).readUInt
+  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
+
+private def ArgumentBufferM.run {α : Type} : ArgumentBufferM α → Native.ArgumentBuffer → IO α :=
+  ReaderT.run
+
+end ArgumentMarshalling
+
 section Proxies
 
 private def MessageDesc.toNative (msg : MessageDesc) : Native.Message :=
@@ -275,8 +314,19 @@ def DisplayM.createObject {ι ι' : InterfaceName} [iface : ResolvedInterface ι
   let proxy ← Native.Proxy.new factory.proxy typeMap ι
   return ⟨proxy⟩
 
--- 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
+/-- Send a request for an object to the server. -/
+def Object.send {ι : InterfaceName} [iface : Interface ι] (obj : Object ι) (req : iface.request) : DisplayM σ Unit := do
+  let argBuffer ← Native.ArgumentBuffer.new
+  let opcode ← ArgumentBufferM.run (iface.requestClass.marshal req) argBuffer
+  obj.proxy.send opcode argBuffer
+
+/-- 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
+    ReaderT.run (handler event) global
+  global.listen obj.proxy actualHandler
 
 end Proxies
 
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index 9eb8398..0e8c079 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -86,7 +86,7 @@ opaque ArgumentBuffer.writeInt : (writer : @& ArgumentBuffer) → (value : Int32
 opaque ArgumentBuffer.writeUInt : (writer : @& ArgumentBuffer) → (value : UInt32) → IO Unit
 
 @[extern "waylean_argument_buffer_write_fixed"]
-opaque ArgumentBuffer.writeFloat : (writer : @& ArgumentBuffer) → (value : Float) → IO Unit
+opaque ArgumentBuffer.writeFixed : (writer : @& ArgumentBuffer) → (value : Float32) → IO Unit
 
 @[extern "waylean_argument_buffer_write_string"]
 opaque ArgumentBuffer.writeString : (writer : @& ArgumentBuffer) → (value : @& Option String) → IO Unit
@@ -107,10 +107,10 @@ opaque ArgumentBuffer.writeFD : (writer : @& ArgumentBuffer) → (value : Int32)
 opaque ArgumentBuffer.readInt : (reader : @& ArgumentBuffer) → IO Int32
 
 @[extern "waylean_argument_buffer_read_uint"]
-opaque ArgumentBuffer.readUInt : (reader : @& ArgumentBuffer) → IO Int32
+opaque ArgumentBuffer.readUInt : (reader : @& ArgumentBuffer) → IO UInt32
 
 @[extern "waylean_argument_buffer_read_fixed"]
-opaque ArgumentBuffer.readFixed : (reader : @& ArgumentBuffer) → IO Float
+opaque ArgumentBuffer.readFixed : (reader : @& ArgumentBuffer) → IO Float32
 
 @[extern "waylean_argument_buffer_read_string"]
 opaque ArgumentBuffer.readString : (reader : @& ArgumentBuffer) → IO (Option String)