diff options
| -rw-r--r-- | lib/CWayland/CWayland.cc | 4 | ||||
| -rw-r--r-- | lib/Wayland/Display.lean | 77 | ||||
| -rw-r--r-- | lib/Wayland/Native.lean | 4 | ||||
| -rw-r--r-- | tools/Scanner/Generator.lean | 80 |
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 |