From ad2c02141844d48e9c50a05f5ce872db283751ce Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Fri, 13 Mar 2026 20:10:14 +0100 Subject: type map implementation --- lib/Wayland/Display.lean | 134 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 134 insertions(+) (limited to 'lib/Wayland/Display.lean') diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 7c628f3..76e5b7d 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -16,9 +16,99 @@ variable {σ α : Type} namespace Wayland +section Interfaces + +/-- The name of an interface (e.g., `"wl_display"`), commonly used to resolve the corresponding interface description +using the `Interface` class. -/ +def InterfaceName : Type := String + deriving Repr, Nonempty, BEq, ToString + +/-- The numeric identifier of a request/event in an interface. -/ +def OpCode : Type := UInt32 + deriving Repr, Nonempty, BEq, OfNat + +/-- Handle to a client object, possibly dead. -/ +structure Object (ι : InterfaceName) where + +/-- Monad in which arguments can be marshalled one after another. -/ +class ArgumentMarshaller (m : Type → Type) extends Monad m where + marshalInt : Int32 → m Unit + marshalUInt : UInt32 → m Unit + marshalFixed : Float32 → m Unit + marshalString : Option String → m Unit + marshalObject {ι : InterfaceName} : Option (Object ι) → m Unit + marshalNewID {ι : InterfaceName} : Object ι → m Unit + marshalArray : ByteArray → m Unit + marshalFD : Int32 → m Unit + +/-- Monad in which arguments can be demarshalled one after another. -/ +class ArgumentDemarshaller (m : Type → Type) extends Monad m where + demarshalInt : m Int32 + demarshalUInt : m UInt32 + demarshalFixed : m Float32 + demarshalString : m (Option String) + demarshalObject {ι : InterfaceName} : m (Option (Object ι)) + demarshalNewID {ι : InterfaceName} : m (Object ι) + demarshalArray : m ByteArray + demarshalFD : m Int32 + +/-- Nullability annotation in an interface's message. -/ +inductive Nullability where + | nullable + | notNull + +/-- Argument description in an interface's message. -/ +inductive ArgumentDesc where + | int : ArgumentDesc + | uint : ArgumentDesc + | fixed : ArgumentDesc + | string : Nullability → ArgumentDesc + | object : Nullability → InterfaceName → ArgumentDesc + | newID : InterfaceName → ArgumentDesc + | array : ArgumentDesc + | fd : ArgumentDesc + +/-- Message description for an interface. -/ +structure MessageDesc where + name : String + args : Array ArgumentDesc + since : UInt32 + isDestructor : Bool + +/-- Class for types describing the request messages of an interface. -/ +class Request (α : Type) where + messages : Array MessageDesc + signature : α → MessageDesc + marshal {m : Type → Type} [ArgumentMarshaller m] : α → m OpCode + +/-- Class for types describing the event messages of an interface. -/ +class Event (α : Type) where + messages : Array MessageDesc + signature : α → MessageDesc + demarshal {m : Type → Type} [ArgumentDemarshaller m] : OpCode → m α + +/-- Class describing an interface. This is not associated with a type, but rather with the interface's name. -/ +class Interface (ι : InterfaceName) where + request : Type + [requestClass : Request request] + event : Type + [eventClass : Event event] + version : UInt32 + +/-- Interface where all dependent interfaces can be resolvew. -/ +class ResolvedInterface (ι : InterfaceName) where + referencedInterfaces : Array ((ι' : InterfaceName) × Interface ι') + contains_self : ∃ α, ⟨ι, α⟩ ∈ referencedInterfaces := by exists inferInstance; simp + -- TODO: Verify that dependencies of interfaces are in referencedInterfaces + +end Interfaces + +section DisplayMonad + /-- A token managing a single source of events such as a timer or a signal handler. This can be used to unregister the event. -/ def EventSource : Type := Native.EventSource + deriving Nonempty /-- Internal handler interface passed as a message to the event loop. -/ private abbrev Handler (σ : Type) := StateT σ IO Unit @@ -26,6 +116,7 @@ private abbrev Handler (σ : Type) := StateT σ IO Unit /-- Access to the display and event loop, providing the main functionality. -/ structure Display (σ : Type) where private disp : Native.Display + private typeMap : Native.TypeMap private addTimer : (delayMs : UInt32) → (msg : Handler σ) → IO EventSource private addSignal : (signum : UInt32) → (msg : Handler σ) → IO EventSource private remove : (source : EventSource) → IO Unit @@ -50,10 +141,12 @@ Parameters: · `name`: Socket name for connecting to the Wayland server (by default, `wayland-0` is used). -/ partial def DisplayM.run' (setUp : DisplayM σ Unit) (initialState : σ) (name : Option String := .none) : IO σ := do let disp ← Native.Display.new name + let typeMap ← Native.TypeMap.new let loop ← Native.EventLoop.new _ ← loop.addDisplay disp let global : Display σ := { disp := disp + typeMap := typeMap addTimer := loop.addTimer addSignal := loop.addSignal remove := loop.remove @@ -125,10 +218,51 @@ def DisplayM.zoom {σ₁ σ₂ : Type} (lens : Lens σ₁ σ₂) (inner : Displa let global₁ : Display σ₁ ← read let global₂ : Display σ₂ := { disp := global₁.disp + typeMap := global₁.typeMap addTimer := fun x y ↦ global₁.addTimer x (zoomState lens y) addSignal := fun x y ↦ global₁.addSignal x (zoomState lens y) remove := global₁.remove quit := global₁.quit } zoomState lens (ReaderT.run inner global₂) +end DisplayMonad + +section Proxies + +private def MessageDesc.toNative (msg : MessageDesc) : Native.Message := + let argString : ArgumentDesc → String + | .int => "i" + | .uint => "u" + | .fixed => "f" + | .string .nullable => "?s" + | .string .notNull => "s" + | .object .nullable _ => "?o" + | .object .notNull _ => "o" + | .newID _ => "n" + | .array => "a" + | .fd => "h" + let argType : ArgumentDesc → Option String + | .object _ iface => .some iface + | .newID iface => .some iface + | _ => .none + { name := msg.name + signature := s!"{msg.since}{String.join (msg.args.toList.map argString)}" + types := msg.args.map argType } + +private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInterface ι] : DisplayM σ Unit := do + let typeMap := (← read).typeMap + for ⟨ι', iface'⟩ in iface.referencedInterfaces do + if !(← typeMap.contains ι') then + typeMap.register + { name := ι' + version := iface'.version + 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 + +end Proxies + end Wayland -- cgit v1.3.1