diff options
Diffstat (limited to 'lib/Wayland')
| -rw-r--r-- | lib/Wayland/Display.lean | 7 | ||||
| -rw-r--r-- | lib/Wayland/Native.lean | 21 |
2 files changed, 25 insertions, 3 deletions
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 76e5b7d..d42147c 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -28,7 +28,8 @@ def OpCode : Type := UInt32 deriving Repr, Nonempty, BEq, OfNat /-- Handle to a client object, possibly dead. -/ -structure Object (ι : InterfaceName) where +def Object (ι : InterfaceName) : Type := Native.Proxy + deriving Nonempty /-- Monad in which arguments can be marshalled one after another. -/ class ArgumentMarshaller (m : Type → Type) extends Monad m where @@ -95,7 +96,7 @@ class Interface (ι : InterfaceName) where [eventClass : Event event] version : UInt32 -/-- Interface where all dependent interfaces can be resolvew. -/ +/-- Interface where all dependency interfaces can be resolvew. -/ class ResolvedInterface (ι : InterfaceName) where referencedInterfaces : Array ((ι' : InterfaceName) × Interface ι') contains_self : ∃ α, ⟨ι, α⟩ ∈ referencedInterfaces := by exists inferInstance; simp @@ -249,6 +250,7 @@ private def MessageDesc.toNative (msg : MessageDesc) : Native.Message := signature := s!"{msg.since}{String.join (msg.args.toList.map argString)}" types := msg.args.map argType } +/-- Ensure the given interface (and all of its dependencies) are registered in the display's `TypeMap`. -/ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInterface ι] : DisplayM σ Unit := do let typeMap := (← read).typeMap for ⟨ι', iface'⟩ in iface.referencedInterfaces do @@ -259,7 +261,6 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter requests := iface'.requestClass.messages.map MessageDesc.toNative events := iface'.eventClass.messages.map MessageDesc.toNative } - -- def Object.send [iface : Interface ι] (obj : Object ι) (req : iface.request) : DisplayM σ Unit := sorry -- def Object.listen [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := sorry diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index e695e5f..f889c25 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -17,16 +17,25 @@ private opaque DisplayP : NonemptyType private opaque EventLoopP (M : Type) : NonemptyType private opaque EventSourceP : NonemptyType private opaque TypeMapP : NonemptyType +private opaque ProxyP : NonemptyType +private opaque ArgumentReaderP : NonemptyType +private opaque ArgumentWriterP : NonemptyType def Display : Type := DisplayP.type def EventLoop (M : Type) : Type := (EventLoopP M).type def EventSource : Type := EventSourceP.type def TypeMap : Type := TypeMapP.type +def Proxy : Type := ProxyP.type +def ArgumentReader : Type := ArgumentReaderP.type +def ArgumentWriter : Type := ArgumentWriterP.type instance : Nonempty Display := DisplayP.property instance : Nonempty (EventLoop M) := (EventLoopP M).property instance : Nonempty EventSource := EventSourceP.property instance : Nonempty TypeMap := TypeMapP.property +instance : Nonempty Proxy := ProxyP.property +instance : Nonempty ArgumentReader := ArgumentReaderP.property +instance : Nonempty ArgumentWriter := ArgumentWriterP.property @[extern "waylean_SIGINT"] opaque SIGINT (u : Unit) : UInt32 @@ -73,4 +82,16 @@ opaque TypeMap.contains : (typeMap : @& TypeMap) → (ifaceName : @& String) → @[extern "waylean_type_map_register"] opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → IO Unit +@[extern "waylean_proxy_from_display"] +opaque Proxy.fromDisplay : (display : @& Display) → IO Proxy + +@[extern "waylean_proxy_new"] +opaque Proxy.new : (factory : @& Proxy) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy + +@[extern "waylean_proxy_send"] +opaque Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentWriter : @& ArgumentWriter) → IO Unit + +@[extern "waylean_proxy_listen"] +opaque Proxy.listen : (proxy : @& Proxy) → (handler : @& (UInt32 → ArgumentReader → EventLoop M × M)) → IO Unit + end Wayland.Native |