native api sketch

2 files changed, 71 insertions, 9 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
 
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index f889c25..909cde4 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -17,25 +17,25 @@ private opaque DisplayP : NonemptyType
 private opaque EventLoopP (M : Type) : NonemptyType
 private opaque EventSourceP : NonemptyType
 private opaque TypeMapP : NonemptyType
-private opaque ProxyP : NonemptyType
 private opaque ArgumentReaderP : NonemptyType
 private opaque ArgumentWriterP : NonemptyType
+private opaque ProxyP : NonemptyType
 
 def Display : Type := DisplayP.type
 def EventLoop (M : Type) : Type := (EventLoopP M).type
 def EventSource : Type := EventSourceP.type
 def TypeMap : Type := TypeMapP.type
-def Proxy : Type := ProxyP.type
 def ArgumentReader : Type := ArgumentReaderP.type
 def ArgumentWriter : Type := ArgumentWriterP.type
+def Proxy : Type := ProxyP.type
 
 instance : Nonempty Display := DisplayP.property
 instance : Nonempty (EventLoop M) := (EventLoopP M).property
 instance : Nonempty EventSource := EventSourceP.property
 instance : Nonempty TypeMap := TypeMapP.property
-instance : Nonempty Proxy := ProxyP.property
 instance : Nonempty ArgumentReader := ArgumentReaderP.property
 instance : Nonempty ArgumentWriter := ArgumentWriterP.property
+instance : Nonempty Proxy := ProxyP.property
 
 @[extern "waylean_SIGINT"]
 opaque SIGINT (u : Unit) : UInt32
@@ -49,9 +49,6 @@ opaque SIGUSR2 (u : Unit) : UInt32
 @[extern "waylean_display_new"]
 opaque Display.new : (name : @& Option String) → IO Display
 
-@[extern "waylean_display_roundtrip"]
-opaque Display.roundtrip : (display : @& Display) → IO Unit
-
 @[extern "waylean_event_loop_new"]
 opaque EventLoop.new : IO (EventLoop M)
 
@@ -82,8 +79,59 @@ opaque TypeMap.contains : (typeMap : @& TypeMap) → (ifaceName : @& String) →
 @[extern "waylean_type_map_register"]
 opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → IO Unit
 
+@[extern "waylean_argument_writer_new"]
+opaque ArgumentWriter.new : IO ArgumentWriter
+
+@[extern "waylean_argument_writer_write_int"]
+opaque ArgumentWriter.writeInt : (writer : @& ArgumentWriter) → (value : Int32) → IO Unit
+
+@[extern "waylean_argument_writer_write_uint"]
+opaque ArgumentWriter.writeUInt : (writer : @& ArgumentWriter) → (value : UInt32) → IO Unit
+
+@[extern "waylean_argument_writer_write_fixed"]
+opaque ArgumentWriter.writeFloat : (writer : @& ArgumentWriter) → (value : Float) → IO Unit
+
+@[extern "waylean_argument_writer_write_string"]
+opaque ArgumentWriter.writeString : (writer : @& ArgumentWriter) → (value : @& Option String) → IO Unit
+
+@[extern "waylean_argument_writer_write_object"]
+opaque ArgumentWriter.writeObject : (writer : @& ArgumentWriter) → (value : @& Option Proxy) → IO Unit
+
+@[extern "waylean_argument_writer_write_new_id"]
+opaque ArgumentWriter.writeNewID : (writer : @& ArgumentWriter) → (value : @& Proxy) → IO Unit
+
+@[extern "waylean_argument_writer_write_array"]
+opaque ArgumentWriter.writeArray : (writer : @& ArgumentWriter) → (value : @& ByteArray) → IO Unit
+
+@[extern "waylean_argument_writer_write_fd"]
+opaque ArgumentWriter.writeFD : (writer : @& ArgumentWriter) → (value : Int32) → IO Unit
+
+@[extern "waylean_argument_reader_read_int"]
+opaque ArgumentReader.readInt : (reader : @& ArgumentReader) → IO Int32
+
+@[extern "waylean_argument_reader_read_uint"]
+opaque ArgumentReader.readUInt : (reader : @& ArgumentReader) → IO Int32
+
+@[extern "waylean_argument_reader_read_fixed"]
+opaque ArgumentReader.readFixed : (reader : @& ArgumentReader) → IO Float
+
+@[extern "waylean_argument_reader_read_string"]
+opaque ArgumentReader.readString : (reader : @& ArgumentReader) → IO (Option String)
+
+@[extern "waylean_argument_reader_read_object"]
+opaque ArgumentReader.readObject : (reader : @& ArgumentReader) → IO (Option Proxy)
+
+@[extern "waylean_argument_reader_read_new_id"]
+opaque ArgumentReader.readNewID : (reader : @& ArgumentReader) → IO UInt32
+
+@[extern "waylean_argument_reader_read_array"]
+opaque ArgumentReader.readArray : (reader : @& ArgumentReader) → IO ByteArray
+
+@[extern "waylean_argument_reader_read_fd"]
+opaque ArgumentReader.readFD : (reader : @& ArgumentReader) → IO Int32
+
 @[extern "waylean_proxy_from_display"]
-opaque Proxy.fromDisplay : (display : @& Display) → IO Proxy
+opaque Proxy.fromDisplay : (display : Display) → IO Proxy
 
 @[extern "waylean_proxy_new"]
 opaque Proxy.new : (factory : @& Proxy) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy
@@ -92,6 +140,6 @@ opaque Proxy.new : (factory : @& Proxy) → (typeMap : @& TypeMap) → (ifaceNam
 opaque Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentWriter : @& ArgumentWriter) → IO Unit
 
 @[extern "waylean_proxy_listen"]
-opaque Proxy.listen : (proxy : @& Proxy) → (handler : @& (UInt32 → ArgumentReader → EventLoop M × M)) → IO Unit
+opaque Proxy.listen : (proxy : @& Proxy) → (handler : UInt32 → ArgumentReader → EventLoop M × M) → IO Unit
 
 end Wayland.Native