type map implementation

3 files changed, 157 insertions, 98 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
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index bd85291..e695e5f 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -2,17 +2,31 @@ variable {M : Type}
 
 namespace Wayland.Native
 
+structure Message where
+  name : String
+  signature : String
+  types : Array (Option String)
+
+structure Interface where
+  name : String
+  version : UInt32
+  requests : Array Message
+  events : Array Message
+
 private opaque DisplayP : NonemptyType
 private opaque EventLoopP (M : Type) : NonemptyType
 private opaque EventSourceP : NonemptyType
+private opaque TypeMapP : NonemptyType
 
 def Display : Type := DisplayP.type
 def EventLoop (M : Type) : Type := (EventLoopP M).type
 def EventSource : Type := EventSourceP.type
+def TypeMap : Type := TypeMapP.type
 
 instance : Nonempty Display := DisplayP.property
 instance : Nonempty (EventLoop M) := (EventLoopP M).property
 instance : Nonempty EventSource := EventSourceP.property
+instance : Nonempty TypeMap := TypeMapP.property
 
 @[extern "waylean_SIGINT"]
 opaque SIGINT (u : Unit) : UInt32
@@ -50,4 +64,13 @@ opaque EventLoop.quit : (eventLoop : @& (EventLoop M)) → IO Unit
 @[extern "waylean_event_loop_poll"]
 opaque EventLoop.poll : (eventLoop : @& (EventLoop M)) → IO (Option M)
 
+@[extern "waylean_type_map_new"]
+opaque TypeMap.new : IO TypeMap
+
+@[extern "waylean_type_map_contains"]
+opaque TypeMap.contains : (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Bool
+
+@[extern "waylean_type_map_register"]
+opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → IO Unit
+
 end Wayland.Native
diff --git a/lib/Wayland/Object.lean b/lib/Wayland/Object.lean
deleted file mode 100644
index 6c5dbb7..0000000
--- a/lib/Wayland/Object.lean
+++ /dev/null
@@ -1,98 +0,0 @@
-import Wayland.Display
-
-namespace Wayland
-
-def InterfaceName : Type := String
-  deriving Repr, BEq
-
-def OpCode : Type := UInt32
-  deriving Repr, BEq
-
-structure Object (ι : InterfaceName) where
-
-structure NewID (ι : InterfaceName) where
-
-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}  : NewID ι           → m Unit
-  marshalArray                      : ByteArray         → m Unit
-  marshalFD                         : Int32             → m Unit
-
-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 (NewID ι)
-  demarshalArray                      : m ByteArray
-  demarshalFD                         : m Int32
-
-inductive Nullability where
-  | nullable
-  | notNull
-
-inductive Argument where
-  | int : Argument
-  | uint : Argument
-  | fixed : Argument
-  | string : Nullability → Argument
-  | object : Nullability → InterfaceName → Argument
-  | newID : InterfaceName → Argument
-  | array : Argument
-  | fd : Argument
-
-structure Message where
-  name : String
-  args : Array Argument
-  since : UInt32
-  isDestructor : Bool
-
-class Request (α : Type) where
-  messages : Array Message
-  signature : α → Message
-  marshal {m : Type → Type} [ArgumentMarshaller m] : α → m OpCode
-
-class Event (α : Type) where
-  messages : Array Message
-  signature : α → Message
-  demarshal {m : Type → Type} [ArgumentDemarshaller m] : OpCode → m α
-
-class Interface (ι : InterfaceName) where
-  request : Type
-  [requestClass : Request request]
-  event : Type
-  [eventClass : Event event]
-  version : UInt32
-
-variable {σ : Type} {ι : InterfaceName}
-
-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
-
--- def WLDisplay.name : InterfaceName := "wl_display"
--- abbrev WLDisplay : Type := Object WLDisplay.name
-
--- inductive WLDisplay.Request where
---   | sync : Request
-
--- inductive WLDisplay.Event where
---   | error : Event
-
--- instance : Request WLDisplay.Request := sorry
--- instance : Event WLDisplay.Event := sorry
--- instance : Interface WLDisplay.name where
---   request := WLDisplay.Request
---   event := WLDisplay.Event
---   version := 1
-
--- def test (disp : WLDisplay) : DisplayM σ Unit := do
---   disp.listen fun
---     | .error => DisplayM.liftIO (IO.println "error!")
---   disp.send .sync
-
-end Wayland