diff options
Diffstat (limited to 'lib/Wayland/Display.lean')
| -rw-r--r-- | lib/Wayland/Display.lean | 43 |
1 files changed, 34 insertions, 9 deletions
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 7bf55c5..9b3b0da 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -32,6 +32,12 @@ structure Object (ι : InterfaceName) : Type where private proxy : Native.Proxy deriving Nonempty +/-- Opaque handle to an object whose type is not statically known. -/ +structure AnyObject : Type where + private proxy : Native.Proxy + private type : String + deriving Nonempty + /-- Monad in which arguments can be marshalled one after another. -/ class ArgumentMarshaller (m : Type → Type) extends Monad m where marshalInt : Int32 → m Unit @@ -39,6 +45,7 @@ class ArgumentMarshaller (m : Type → Type) extends Monad m where marshalFixed : Float32 → m Unit marshalString : Option String → m Unit marshalObject {ι : InterfaceName} : Option (Object ι) → m Unit + marshalAnyObject : Option AnyObject → m Unit marshalArray : ByteArray → m Unit marshalFD : Int32 → m Unit @@ -49,6 +56,7 @@ class ArgumentDemarshaller (m : Type → Type) extends Monad m where demarshalFixed : m Float32 demarshalString : m (Option String) demarshalObject {ι : InterfaceName} : m (Option (Object ι)) + demarshalAnyObject : m (Option AnyObject) demarshalArray : m ByteArray demarshalFD : m Int32 @@ -63,8 +71,8 @@ inductive ArgumentDesc where | uint : ArgumentDesc | fixed : ArgumentDesc | string : Nullability → ArgumentDesc - | object : Nullability → InterfaceName → ArgumentDesc - | newID : InterfaceName → ArgumentDesc + | object : Nullability → (Option InterfaceName) → ArgumentDesc + | newID : (Option InterfaceName) → ArgumentDesc | array : ArgumentDesc | fd : ArgumentDesc @@ -239,6 +247,7 @@ private instance : ArgumentMarshaller ArgumentBufferM where marshalFixed v := do (← read).writeFixed v marshalString v := do (← read).writeString v 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 @@ -247,7 +256,13 @@ private instance : ArgumentDemarshaller ArgumentBufferM where demarshalUInt := do (← read).readUInt demarshalFixed := do (← read).readFixed demarshalString := do (← read).readString - demarshalObject := do let proxy ← (← read).readObject; return proxy.map Object.mk + demarshalObject := do + let proxy ← (← read).readObject + return proxy.map Object.mk + demarshalAnyObject := do + let proxy ← (← read).readObject + proxy.mapM fun proxy ↦ do + return ⟨proxy, ← proxy.getType⟩ demarshalArray := do (← read).readArray demarshalFD := do (← read).readFD @@ -271,8 +286,8 @@ private def MessageDesc.toNative (msg : MessageDesc) : Native.Message := | .array => "a" | .fd => "h" let argType : ArgumentDesc → Option String - | .object _ iface => .some iface - | .newID iface => .some iface + | .object _ iface => iface + | .newID iface => iface | _ => .none { name := msg.name signature := s!"{msg.since}{String.join (msg.args.toList.map argString)}" @@ -295,14 +310,16 @@ def DisplayM.getDisplay : DisplayM σ (Object "wl_display") := do let proxy ← Native.Proxy.fromDisplay (← read).disp return ⟨proxy⟩ +variable {ι ι' : InterfaceName} + /-- Send a request for an object to the server that doesn't construct any new object. -/ -def Object.send {ι : InterfaceName} (obj : Object ι) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ Unit := do +def Object.send (obj : Object ι) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ Unit := do let argBuffer ← Native.ArgumentBuffer.new let opcode ← ArgumentBufferM.run marshaller argBuffer 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 {ι ι' : InterfaceName} [iface : ResolvedInterface ι'] (obj : Object ι) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ (Object ι') := do +def Object.sendConstructor [iface : ResolvedInterface ι'] (obj : Object ι) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ (Object ι') := do DisplayM.ensureInterface ι' let typeMap := (← read).typeMap let argBuffer ← Native.ArgumentBuffer.new @@ -311,7 +328,7 @@ def Object.sendConstructor {ι ι' : InterfaceName} [iface : ResolvedInterface return ⟨proxy⟩ /-- 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 +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 @@ -319,9 +336,17 @@ def Object.listen {ι : InterfaceName} [iface : Interface ι] (obj : Object ι) global.listen obj.proxy actualHandler /-- Shorthand to ensure the reference count of an `Object` does not drop to `0`. -/ -def Object.keep {ι : InterfaceName} (obj : Object ι) : DisplayM σ Unit := +def Object.keep (obj : Object ι) : DisplayM σ Unit := obj.proxy.keep +/-- Erase the type information from an object. -/ +def Object.toAny (obj : Object ι) : AnyObject := + ⟨obj.proxy, ι⟩ + +/-- Try to cast a type-erased object into a typed object. -/ +def AnyObject.cast (obj : AnyObject) : Option (Object ι) := + if obj.type == ι then .some ⟨obj.proxy⟩ else .none + end Proxies end Wayland |