basic argument (de-)marshalling

2 files changed, 72 insertions, 9 deletions

diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 9b3b0da..9ba60bc 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -27,6 +27,10 @@ def InterfaceName : Type := String
 def OpCode : Type := UInt32
   deriving Repr, Nonempty, BEq, OfNat, DecidableEq
 
+/-- A POSIX file descriptor. -/
+def Fd : Type := Int32
+  deriving Repr, Nonempty, BEq, DecidableEq
+
 /-- Handle to a client object, possibly dead. -/
 structure Object (ι : InterfaceName) : Type where
   private proxy : Native.Proxy
@@ -47,10 +51,10 @@ class ArgumentMarshaller (m : Type → Type) extends Monad m where
   marshalObject {ι : InterfaceName} : Option (Object ι) → m Unit
   marshalAnyObject                  : Option AnyObject  → m Unit
   marshalArray                      : ByteArray         → m Unit
-  marshalFD                         : Int32             → m Unit
+  marshalFd                         : Fd                → m Unit
 
 /-- Monad in which arguments can be demarshalled one after another. -/
-class ArgumentDemarshaller (m : Type → Type) extends Monad m where
+class ArgumentDemarshaller (m : Type → Type) extends Monad m, MonadExcept String m where
   demarshalInt                        : m Int32
   demarshalUInt                       : m UInt32
   demarshalFixed                      : m Float32
@@ -58,7 +62,12 @@ class ArgumentDemarshaller (m : Type → Type) extends Monad m where
   demarshalObject {ι : InterfaceName} : m (Option (Object ι))
   demarshalAnyObject                  : m (Option AnyObject)
   demarshalArray                      : m ByteArray
-  demarshalFD                         : m Int32
+  demarshalFd                         : m Fd
+
+/-- A type is `Marshallable` if it can be marshalled and demarshalled using a corresponding monad. -/
+class Marshallable (α : Type) where
+  marshal {m : Type → Type} [ArgumentMarshaller m] : α → m Unit
+  demarshal {m : Type → Type} [ArgumentDemarshaller m] : m α
 
 /-- Nullability annotation in an interface's message. -/
 inductive Nullability where
@@ -249,9 +258,9 @@ private instance : ArgumentMarshaller ArgumentBufferM where
   marshalObject v := do (← read).writeObject (v.map Object.proxy)
   marshalAnyObject v := do (← read).writeObject (v.map AnyObject.proxy)
   marshalArray v := do (← read).writeArray v
-  marshalFD v := do (← read).writeFD v
+  marshalFd v := do (← read).writeFd v
 
-private instance : ArgumentDemarshaller ArgumentBufferM where
+private instance : ArgumentDemarshaller (ExceptT String ArgumentBufferM) where
   demarshalInt := do (← read).readInt
   demarshalUInt := do (← read).readUInt
   demarshalFixed := do (← read).readFixed
@@ -264,11 +273,64 @@ private instance : ArgumentDemarshaller ArgumentBufferM where
     proxy.mapM fun proxy ↦ do
       return ⟨proxy, ← proxy.getType⟩
   demarshalArray := do (← read).readArray
-  demarshalFD := do (← read).readFD
+  demarshalFd := do (← read).readFd
 
 private def ArgumentBufferM.run {α : Type} : ArgumentBufferM α → Native.ArgumentBuffer → IO α :=
   ReaderT.run
 
+instance : Marshallable Int32 where
+  marshal := ArgumentMarshaller.marshalInt
+  demarshal := ArgumentDemarshaller.demarshalInt
+
+instance : Marshallable UInt32 where
+  marshal := ArgumentMarshaller.marshalUInt
+  demarshal := ArgumentDemarshaller.demarshalUInt
+
+instance : Marshallable Float32 where
+  marshal := ArgumentMarshaller.marshalFixed
+  demarshal := ArgumentDemarshaller.demarshalFixed
+
+instance : Marshallable (Option String) where
+  marshal := ArgumentMarshaller.marshalString
+  demarshal := ArgumentDemarshaller.demarshalString
+
+instance (ι : InterfaceName) : Marshallable (Option (Object ι)) where
+  marshal := ArgumentMarshaller.marshalObject
+  demarshal := ArgumentDemarshaller.demarshalObject
+
+instance : Marshallable (Option AnyObject) where
+  marshal := ArgumentMarshaller.marshalAnyObject
+  demarshal := ArgumentDemarshaller.demarshalAnyObject
+
+instance : Marshallable ByteArray where
+  marshal := ArgumentMarshaller.marshalArray
+  demarshal := ArgumentDemarshaller.demarshalArray
+
+instance : Marshallable Fd where
+  marshal := ArgumentMarshaller.marshalFd
+  demarshal := ArgumentDemarshaller.demarshalFd
+
+instance : Marshallable String where
+  marshal s := Marshallable.marshal (Option.some s)
+  demarshal := do
+    match ((← Marshallable.demarshal) : Option String) with
+    | .some s => pure s
+    | .none   => throw "Received null for a non-nullable string."
+
+instance (ι : InterfaceName) : Marshallable (Object ι) where
+  marshal o := Marshallable.marshal (Option.some o)
+  demarshal := do
+    match ((← Marshallable.demarshal) : Option (Object ι)) with
+    | .some o => pure o
+    | .none   => throw "Received null for a non-nullable object."
+
+instance : Marshallable AnyObject where
+  marshal o := Marshallable.marshal (Option.some o)
+  demarshal := do
+    match ((← Marshallable.demarshal) : Option AnyObject) with
+    | .some o => pure o
+    | .none   => throw "Received null for a non-nullable object."
+
 end ArgumentMarshalling
 
 section Proxies
@@ -331,7 +393,8 @@ def Object.sendConstructor [iface : ResolvedInterface ι'] (obj : Object ι) (ma
 def Object.listen [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.demarshalEvent opcode) argBuffer
+    let event : Except String iface.event ← ArgumentBufferM.run (ExceptT.run (iface.demarshalEvent opcode)) argBuffer
+    let event : iface.event ← IO.ofExcept event
     ReaderT.run (handler event) global
   global.listen obj.proxy actualHandler
 
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index 25884ed..b4e9e95 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -101,7 +101,7 @@ opaque ArgumentBuffer.writeObject : (writer : @& ArgumentBuffer) → (value : @&
 opaque ArgumentBuffer.writeArray : (writer : @& ArgumentBuffer) → (value : @& ByteArray) → IO Unit
 
 @[extern "waylean_argument_buffer_write_fd"]
-opaque ArgumentBuffer.writeFD : (writer : @& ArgumentBuffer) → (value : Int32) → IO Unit
+opaque ArgumentBuffer.writeFd : (writer : @& ArgumentBuffer) → (value : Int32) → IO Unit
 
 @[extern "waylean_argument_buffer_read_int"]
 opaque ArgumentBuffer.readInt : (reader : @& ArgumentBuffer) → IO Int32
@@ -122,7 +122,7 @@ opaque ArgumentBuffer.readObject : (reader : @& ArgumentBuffer) → IO (Option P
 opaque ArgumentBuffer.readArray : (reader : @& ArgumentBuffer) → IO ByteArray
 
 @[extern "waylean_argument_buffer_read_fd"]
-opaque ArgumentBuffer.readFD : (reader : @& ArgumentBuffer) → IO Int32
+opaque ArgumentBuffer.readFd : (reader : @& ArgumentBuffer) → IO Int32
 
 @[extern "waylean_proxy_from_display"]
 opaque Proxy.fromDisplay : (display : Display) → IO Proxy