diff options
Diffstat (limited to 'lib/Wayland/Display.lean')
| -rw-r--r-- | lib/Wayland/Display.lean | 77 |
1 files changed, 70 insertions, 7 deletions
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 |