basic argument (de-)marshalling

4 files changed, 117 insertions, 48 deletions

diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc
index 0c02d66..3487f72 100644
--- a/lib/CWayland/CWayland.cc
+++ b/lib/CWayland/CWayland.cc
@@ -1109,7 +1109,7 @@ lean_obj_res waylean_argument_buffer_write_array(b_lean_obj_arg buffer_obj, b_le
     return lean_io_result_mk_ok(lean_box(0));
 }
 
-// ArgumentBuffer.writeFD : (buffer : @& ArgumentBuffer) → (value : Int32) → IO Unit
+// ArgumentBuffer.writeFd : (buffer : @& ArgumentBuffer) → (value : Int32) → IO Unit
 lean_obj_res waylean_argument_buffer_write_fd(b_lean_obj_arg buffer_obj, int32_t value)
 {
     auto buffer = static_cast<argument_buffer*>(lean_get_external_data(buffer_obj));
@@ -1159,7 +1159,7 @@ lean_obj_res waylean_argument_buffer_read_array(b_lean_obj_arg buffer_obj)
     return lean_io_result_mk_ok(buffer->read_array().release());
 }
 
-// ArgumentBuffer.readFD : (buffer : @& ArgumentBuffer) → IO Int32
+// ArgumentBuffer.readFd : (buffer : @& ArgumentBuffer) → IO Int32
 lean_obj_res waylean_argument_buffer_read_fd(b_lean_obj_arg buffer_obj)
 {
     auto buffer = static_cast<argument_buffer*>(lean_get_external_data(buffer_obj));
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
diff --git a/tools/Scanner/Generator.lean b/tools/Scanner/Generator.lean
index 5884a0d..1f889d0 100644
--- a/tools/Scanner/Generator.lean
+++ b/tools/Scanner/Generator.lean
@@ -68,6 +68,21 @@ private def resolveEnum (enum : EnumRef) : Generator String := do
   let iface ← resolveInterface enum.toInterfaceRef
   return s!"{iface}.{enum.enum.pascalCase}"
 
+private def typeToLean : ArgumentType → Generator String
+  | .int .none                      => do return "Int32"
+  | .int (.some enum)               => resolveEnum enum
+  | .uint .none                     => do return "UInt32"
+  | .uint (.some enum)              => resolveEnum enum
+  | .fixed                          => do return "Float32"
+  | .string .nullable               => do return "Option String"
+  | .string .notNull                => do return "String"
+  | .array                          => do return "ByteArray"
+  | .fd                             => do return "Fd"
+  | .object .nullable .none         => do return "Option AnyObject"
+  | .object .nullable (.some iface) => do return s!"Option {← resolveInterface iface}"
+  | .object .notNull  .none         => do return s!"AnyObject"
+  | .object .notNull  (.some iface) => resolveInterface iface
+
 section Header
 
 private def emitNameDefinitions (protocol : ProtocolDesc) : Generator Unit := do
@@ -76,7 +91,7 @@ private def emitNameDefinitions (protocol : ProtocolDesc) : Generator Unit := do
 
 private def emitObjectDefinitions (protocol : ProtocolDesc) : Generator Unit := do
   for iface in protocol.interfaces do
-    emitLine s!"def {iface.name.pascalCase} : Type := Object {iface.name.pascalCase}.name"
+    emitLine s!"abbrev {iface.name.pascalCase} : Type := Object {iface.name.pascalCase}.name"
 
 private def emitEnumDefinitions (protocol : ProtocolDesc) : Generator Unit := do
   for iface in protocol.interfaces do
@@ -91,6 +106,15 @@ private def emitEnumDefinitions (protocol : ProtocolDesc) : Generator Unit := do
         for entry in enum.entries do
           emitLine s!"  | {entry.name.camelCase}"
 
+private def emitEnumMarshallable (protocol : ProtocolDesc) : Generator Unit := do
+  for iface in protocol.interfaces do
+    for enum in iface.enums do
+      emitLine s!""
+      emitLine s!"instance : Marshallable {iface.name.pascalCase}.{enum.name.pascalCase} where"
+      emitLine s!"  marshal := sorry"
+      emitLine s!"  demarshal := sorry"
+      -- TODO
+
 def generateHeader (rootModule : String) (protocol : ProtocolDesc) : String :=
   Generator.runProtocol rootModule protocol ".Header" do
     emitNamespace rootModule do
@@ -99,6 +123,7 @@ def generateHeader (rootModule : String) (protocol : ProtocolDesc) : String :=
       emitLine ""
       emitObjectDefinitions protocol
       emitEnumDefinitions protocol
+      emitEnumMarshallable protocol
 
 end Header
 
@@ -110,21 +135,7 @@ private def emitEventDefinitions (protocol : ProtocolDesc) : Generator Unit := d
     for event in iface.events do
       emitLine s!"  | {event.name.camelCase}"
       for arg in event.arguments do
-        let argName := arg.name.camelCase
-        match arg.type with
-          | .int .none                      => emitLine s!"    ({argName} : Int32)"
-          | .int (.some enum)               => emitLine s!"    ({argName} : {← resolveEnum enum})"
-          | .uint .none                     => emitLine s!"    ({argName} : UInt32)"
-          | .uint (.some enum)              => emitLine s!"    ({argName} : {← resolveEnum enum})"
-          | .fixed                          => emitLine s!"    ({argName} : Float)"
-          | .string .nullable               => emitLine s!"    ({argName} : Option String)"
-          | .string .notNull                => emitLine s!"    ({argName} : String)"
-          | .array                          => emitLine s!"    ({argName} : ByteArray)"
-          | .fd                             => emitLine s!"    ({argName} : Int32)"
-          | .object .nullable .none         => emitLine s!"    ({argName} : Option AnyObject)"
-          | .object .nullable (.some iface) => emitLine s!"    ({argName} : Option {← resolveInterface iface})"
-          | .object .notNull  .none         => emitLine s!"    ({argName} : AnyObject)"
-          | .object .notNull  (.some iface) => emitLine s!"    ({argName} : {← resolveInterface iface})"
+        emitLine s!"    ({arg.name.camelCase} : {← typeToLean arg.type})"
     emitLine s!""
 
 private def emitInterfaceInstances (protocol : ProtocolDesc) : Generator Unit := do
@@ -168,8 +179,13 @@ private def emitInterfaceInstances (protocol : ProtocolDesc) : Generator Unit :=
     for ev in iface.events do
       emitMessageDesc ev.toMessageDesc
     emitLine s!"  ]"
-    emitLine s!"  demarshalEvent := sorry"
-    -- TODO
+    emitLine s!"  demarshalEvent"
+    for ev in iface.events do
+      emitLine s!"    | {ev.opcode} => do"
+      emitLine s!"      return .{ev.name.camelCase}"
+      for _ in ev.arguments do
+        emitLine s!"        (← Marshallable.demarshal)"
+    emitLine "    | _ => throw s!\"Received invalid opcode\""
 
 def generateInterface (rootModule : String) (protocol : ProtocolDesc) : String :=
   Generator.runProtocol rootModule protocol ".Interface" do
@@ -212,34 +228,24 @@ private def emitRequests (protocol : ProtocolDesc) : Generator Unit := do
       emitLine s!"    (ω : {iface.name.pascalCase})"
       -- TODO: Special wl_callback handling
       for arg in req.arguments do
-        let argName := arg.name.camelCase
-        match arg.type with
-          | .int .none                      => emitLine s!"    ({argName} : Int32)"
-          | .int (.some enum)               => emitLine s!"    ({argName} : {← resolveEnum enum})"
-          | .uint .none                     => emitLine s!"    ({argName} : UInt32)"
-          | .uint (.some enum)              => emitLine s!"    ({argName} : {← resolveEnum enum})"
-          | .fixed                          => emitLine s!"    ({argName} : Float)"
-          | .string .nullable               => emitLine s!"    ({argName} : Option String)"
-          | .string .notNull                => emitLine s!"    ({argName} : String)"
-          | .array                          => emitLine s!"    ({argName} : ByteArray)"
-          | .fd                             => emitLine s!"    ({argName} : Int32)"
-          | .object .nullable .none         => emitLine s!"    ({argName} : Option AnyObject)"
-          | .object .nullable (.some iface) => emitLine s!"    ({argName} : Option {← resolveInterface iface (suffix := ".Resolved")})"
-          | .object .notNull  .none         => emitLine s!"    ({argName} : AnyObject)"
-          | .object .notNull  (.some iface) => emitLine s!"    ({argName} : {← resolveInterface iface (suffix := ".Resolved")})"
+        emitLine s!"    ({arg.name.camelCase} : {← typeToLean arg.type})"
       match req.returnType with
         | .unit                 => emitLine s!"    : DisplayM σ Unit :="
-        | .object .none         => emitLine s!"    : DisplayM σ AnyObject :="
+        | .object .none         => emitLine s!"    : DisplayM σ (Object ι) :="
         | .object (.some iface) => emitLine s!"    : DisplayM σ {← resolveInterface iface (suffix := ".Resolved")} :="
-      emitLine s!"  sorry"
-      -- TODO
+      match req.returnType with
+        | .unit     => emitLine s!"  ω.send do"
+        | .object _ => emitLine s!"  ω.sendConstructor do"
+      for arg in req.arguments do
+        emitLine s!"    Marshallable.marshal {arg.name.camelCase}"
+      emitLine s!"    return {req.opcode}"
 
 def generateRequests (rootModule : String) (protocol : ProtocolDesc) : String :=
   Generator.runProtocol rootModule protocol ".Requests" do
     emitNamespace rootModule do
       emitImport "Wayland.Display"
       emitLocalImport protocol.name ".Resolved"
-      emitLine "variable {σ : Type}"
+      emitLine "variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]"
       emitRequests protocol
 
 end Requests