1 files changed, 134 insertions, 0 deletions
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