native api sketch

1 files changed, 15 insertions, 1 deletions

diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index d42147c..2e2ceaa 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. -/
-def Object (ι : InterfaceName) : Type := Native.Proxy
+structure Object (ι : InterfaceName) : Type where
+  private proxy : Native.Proxy
   deriving Nonempty
 
 /-- Monad in which arguments can be marshalled one after another. -/
@@ -261,6 +262,19 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter
           requests := iface'.requestClass.messages.map MessageDesc.toNative
           events := iface'.eventClass.messages.map MessageDesc.toNative }
 
+/-- Get the `wl_display` instance within the display monad. -/
+def DisplayM.getDisplay : DisplayM σ (Object "wl_display") := do
+  let proxy ← Native.Proxy.fromDisplay (← read).disp
+  return ⟨proxy⟩
+
+/-- Create a new object, allocating a new ID in the client space and inheriting the display from the `factory`
+object. -/
+def DisplayM.createObject {ι ι' : InterfaceName} [iface : ResolvedInterface ι] (factory : Object ι') : DisplayM σ (Object ι) := do
+  ensureInterface ι
+  let typeMap := (← read).typeMap
+  let proxy ← Native.Proxy.new factory.proxy typeMap ι
+  return ⟨proxy⟩
+
 -- 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