native api sketch

1 files changed, 56 insertions, 8 deletions

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