diff options
| -rw-r--r-- | lib/Wayland/Display.lean | 112 | ||||
| -rw-r--r-- | tools/Scanner/Generator.lean | 51 |
2 files changed, 124 insertions, 39 deletions
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 70f5c67..63bd70d 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -43,7 +43,7 @@ structure AnyObject : Type where deriving Nonempty /-- Monad in which arguments can be marshalled one after another. -/ -class ArgumentMarshaller (m : Type → Type) extends Monad m where +class ArgumentMarshaller (m : Type → Type) extends Monad m, MonadExcept String m where marshalInt : Int32 → m Unit marshalUInt : UInt32 → m Unit marshalFixed : Float32 → m Unit @@ -64,10 +64,20 @@ class ArgumentDemarshaller (m : Type → Type) extends Monad m, MonadExcept Stri demarshalArray : m ByteArray demarshalFd : m Fd +/-- Argument description in an interface's message. -/ +inductive MarshalType where + | int + | uint + | fixed + | string + | object + | array + | 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 α + marshal {m : Type → Type} [ArgumentMarshaller m] : MarshalType → α → m Unit + demarshal {m : Type → Type} [ArgumentDemarshaller m] : MarshalType → m α /-- Nullability annotation in an interface's message. -/ inductive Nullability where @@ -250,7 +260,7 @@ deriving instance Monad for ArgumentBufferM private instance : MonadLift (ReaderT Native.ArgumentBuffer IO) ArgumentBufferM where monadLift := id -private instance : ArgumentMarshaller ArgumentBufferM where +private instance : ArgumentMarshaller (ExceptT String ArgumentBufferM) where marshalInt v := do (← read).writeInt v marshalUInt v := do (← read).writeUInt v marshalFixed v := do (← read).writeFixed v @@ -279,55 +289,87 @@ private def ArgumentBufferM.run {α : Type} : ArgumentBufferM α → Native.Argu ReaderT.run instance : Marshallable Int32 where - marshal := ArgumentMarshaller.marshalInt - demarshal := ArgumentDemarshaller.demarshalInt + marshal + | .int => ArgumentMarshaller.marshalInt + | _ => fun _ ↦ throw "Marshalling unexpected type, expected int." + demarshal + | .int => ArgumentDemarshaller.demarshalInt + | _ => throw "Demarshalling unexpected type, expected int." instance : Marshallable UInt32 where - marshal := ArgumentMarshaller.marshalUInt - demarshal := ArgumentDemarshaller.demarshalUInt + marshal + | .uint => ArgumentMarshaller.marshalUInt + | _ => fun _ ↦ throw "Marshalling unexpected type, expected uint." + demarshal + | .uint => ArgumentDemarshaller.demarshalUInt + | _ => throw "Demarshalling unexpected type, expected uint." instance : Marshallable Float32 where - marshal := ArgumentMarshaller.marshalFixed - demarshal := ArgumentDemarshaller.demarshalFixed + marshal + | .fixed => ArgumentMarshaller.marshalFixed + | _ => fun _ ↦ throw "Marshalling unexpected type, expected fixed." + demarshal + | .fixed => ArgumentDemarshaller.demarshalFixed + | _ => throw "Demarshalling unexpected type, expected fixed." instance : Marshallable (Option String) where - marshal := ArgumentMarshaller.marshalString - demarshal := ArgumentDemarshaller.demarshalString + marshal + | .string => ArgumentMarshaller.marshalString + | _ => fun _ ↦ throw "Marshalling unexpected type, expected string." + demarshal + | .string => ArgumentDemarshaller.demarshalString + | _ => throw "Demarshalling unexpected type, expected string." instance (ι : InterfaceName) : Marshallable (Option (Object ι)) where - marshal := ArgumentMarshaller.marshalObject - demarshal := ArgumentDemarshaller.demarshalObject + marshal + | .object => ArgumentMarshaller.marshalObject + | _ => fun _ ↦ throw "Marshalling unexpected type, expected object." + demarshal + | .object => ArgumentDemarshaller.demarshalObject + | _ => throw "Demarshalling unexpected type, expected object." instance : Marshallable (Option AnyObject) where - marshal := ArgumentMarshaller.marshalAnyObject - demarshal := ArgumentDemarshaller.demarshalAnyObject + marshal + | .object => ArgumentMarshaller.marshalAnyObject + | _ => fun _ ↦ throw "Marshalling unexpected type, expected object." + demarshal + | .object => ArgumentDemarshaller.demarshalAnyObject + | _ => throw "Demarshalling unexpected type, expected object." instance : Marshallable ByteArray where - marshal := ArgumentMarshaller.marshalArray - demarshal := ArgumentDemarshaller.demarshalArray + marshal + | .array => ArgumentMarshaller.marshalArray + | _ => fun _ ↦ throw "Marshalling unexpected type, expected array." + demarshal + | .array => ArgumentDemarshaller.demarshalArray + | _ => throw "Demarshalling unexpected type, expected array." instance : Marshallable Fd where - marshal := ArgumentMarshaller.marshalFd - demarshal := ArgumentDemarshaller.demarshalFd + marshal + | .fd => ArgumentMarshaller.marshalFd + | _ => fun _ ↦ throw "Marshalling unexpected type, expected fd." + demarshal + | .fd => ArgumentDemarshaller.demarshalFd + | _ => throw "Demarshalling unexpected type, expected fd." instance : Marshallable String where - marshal s := Marshallable.marshal (Option.some s) - demarshal := do - match ((← Marshallable.demarshal) : Option String) with + marshal a s := Marshallable.marshal a (Option.some s) + demarshal a := do + match ((← Marshallable.demarshal a) : 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 + marshal a o := Marshallable.marshal a (Option.some o) + demarshal a := do + match ((← Marshallable.demarshal a) : 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 + marshal a o := Marshallable.marshal a (Option.some o) + demarshal a := do + match ((← Marshallable.demarshal a) : Option AnyObject) with | .some o => pure o | .none => throw "Received null for a non-nullable object." @@ -373,18 +415,22 @@ def DisplayM.getDisplay' : DisplayM σ (Object "wl_display") := do variable {ι ι' : InterfaceName} +private def marshalArguments (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : IO (Native.ArgumentBuffer × OpCode) := do + let argBuffer ← Native.ArgumentBuffer.new + let opcode : Except String OpCode ← ArgumentBufferM.run (ExceptT.run marshaller) argBuffer + let opcode : OpCode ← IO.ofExcept opcode + return (argBuffer, opcode) + /-- Send a request for an object to the server that doesn't construct any new object. -/ def Object.send (obj : Object ι) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ Unit := do - let argBuffer ← Native.ArgumentBuffer.new - let opcode ← ArgumentBufferM.run marshaller argBuffer + let (argBuffer, opcode) ← marshalArguments marshaller 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 [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 (argBuffer, opcode) ← marshalArguments marshaller let proxy ← obj.proxy.sendConstructor opcode argBuffer typeMap ι' return ⟨proxy⟩ diff --git a/tools/Scanner/Generator.lean b/tools/Scanner/Generator.lean index 76542e7..f2514f4 100644 --- a/tools/Scanner/Generator.lean +++ b/tools/Scanner/Generator.lean @@ -85,6 +85,16 @@ private def typeToLean : ArgumentType → Generator String | .newID .none => do return s!"AnyObject" | .newID (.some iface) => resolveInterface iface +private def marshalType : ArgumentType → String + | .int _ => ".int" + | .uint _ => ".uint" + | .fixed => ".fixed" + | .string _ => ".string" + | .object _ _ => ".object" + | .newID _ => ".object" + | .array => ".array" + | .fd => ".fd" + section Header private def emitNameDefinitions (protocol : ProtocolDesc) : Generator Unit := do @@ -113,9 +123,38 @@ private def emitEnumMarshallable (protocol : ProtocolDesc) : Generator Unit := d 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 + if enum.bitfield then + emitLine s!" marshal" + emitLine s!" | .uint, μ => ArgumentMarshaller.marshalUInt <|" + emitLine s!" 0" + for entry in enum.entries do + emitLine s!" ||| (if μ.{entry.name.camelCase} then {entry.value} else 0)" + emitLine s!" | _, _ => throw \"Marshalling unexpected type, expected uint.\"" + emitLine s!" demarshal" + emitLine s!" | .uint => do" + emitLine s!" let μ ← ArgumentDemarshaller.demarshalUInt" + emitLine " return {" + for entry in enum.entries do + emitLine s!" {entry.name.camelCase} := (μ &&& {entry.value}) == {entry.value}" + emitLine " }" + emitLine s!" | _ => throw \"Demarshalling unexpected type, expected uint.\"" + else + emitLine s!" marshal" + for entry in enum.entries do + emitLine s!" | .int, .{entry.name.camelCase} => ArgumentMarshaller.marshalInt {entry.value}" + emitLine s!" | .uint, .{entry.name.camelCase} => ArgumentMarshaller.marshalUInt {entry.value}" + emitLine s!" | _, _ => throw \"Marshalling unexpected type, expected int or uint.\"" + emitLine s!" demarshal" + let emitMatch (demarshal : String) : Generator Unit := do + emitLine s!" match (← ArgumentDemarshaller.{demarshal}) with" + for entry in enum.entries do + emitLine s!" | {entry.value} => pure .{entry.name.camelCase}" + emitLine s!" | _ => throw \"Invalid enum value.\"" + emitLine s!" | .int => do" + emitMatch "demarshalInt" + emitLine s!" | .uint => do" + emitMatch "demarshalUInt" + emitLine s!" | _ => throw \"Demarshalling unexpected type, expected int or uint.\"" def generateHeader (rootModule : String) (protocol : ProtocolDesc) : String := Generator.runProtocol rootModule protocol ".Header" do @@ -186,8 +225,8 @@ private def emitInterfaceInstances (protocol : ProtocolDesc) : Generator Unit := 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)" + for arg in ev.arguments do + emitLine s!" (← Marshallable.demarshal {marshalType arg.type})" emitLine " | _ => throw s!\"Received invalid opcode\"" def generateInterface (rootModule : String) (protocol : ProtocolDesc) : String := @@ -252,7 +291,7 @@ private def emitRequests (protocol : ProtocolDesc) : Generator Unit := do emitLine s!" ArgumentMarshaller.marshalUInt (inferInstanceAs (Interface ι)).version" emitLine s!" ArgumentMarshaller.marshalAnyObject .none" | _ => - emitLine s!" Marshallable.marshal {arg.name.camelCase}" + emitLine s!" Marshallable.marshal {marshalType arg.type} {arg.name.camelCase}" emitLine s!" return {req.opcode}" -- Special case wl_callback handling if req.returnType.isWlCallback then |