clean up argument buffers

1 files changed, 39 insertions, 42 deletions

diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index 909cde4..9eb8398 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -17,24 +17,21 @@ private opaque DisplayP : NonemptyType
 private opaque EventLoopP (M : Type) : NonemptyType
 private opaque EventSourceP : NonemptyType
 private opaque TypeMapP : NonemptyType
-private opaque ArgumentReaderP : NonemptyType
-private opaque ArgumentWriterP : NonemptyType
+private opaque ArgumentBufferP : 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 ArgumentReader : Type := ArgumentReaderP.type
-def ArgumentWriter : Type := ArgumentWriterP.type
+def ArgumentBuffer : Type := ArgumentBufferP.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 ArgumentReader := ArgumentReaderP.property
-instance : Nonempty ArgumentWriter := ArgumentWriterP.property
+instance : Nonempty ArgumentBuffer := ArgumentBufferP.property
 instance : Nonempty Proxy := ProxyP.property
 
 @[extern "waylean_SIGINT"]
@@ -79,56 +76,56 @@ 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_buffer_new"]
+opaque ArgumentBuffer.new : IO ArgumentBuffer
 
-@[extern "waylean_argument_writer_write_int"]
-opaque ArgumentWriter.writeInt : (writer : @& ArgumentWriter) → (value : Int32) → IO Unit
+@[extern "waylean_argument_buffer_write_int"]
+opaque ArgumentBuffer.writeInt : (writer : @& ArgumentBuffer) → (value : Int32) → IO Unit
 
-@[extern "waylean_argument_writer_write_uint"]
-opaque ArgumentWriter.writeUInt : (writer : @& ArgumentWriter) → (value : UInt32) → IO Unit
+@[extern "waylean_argument_buffer_write_uint"]
+opaque ArgumentBuffer.writeUInt : (writer : @& ArgumentBuffer) → (value : UInt32) → IO Unit
 
-@[extern "waylean_argument_writer_write_fixed"]
-opaque ArgumentWriter.writeFloat : (writer : @& ArgumentWriter) → (value : Float) → IO Unit
+@[extern "waylean_argument_buffer_write_fixed"]
+opaque ArgumentBuffer.writeFloat : (writer : @& ArgumentBuffer) → (value : Float) → IO Unit
 
-@[extern "waylean_argument_writer_write_string"]
-opaque ArgumentWriter.writeString : (writer : @& ArgumentWriter) → (value : @& Option String) → IO Unit
+@[extern "waylean_argument_buffer_write_string"]
+opaque ArgumentBuffer.writeString : (writer : @& ArgumentBuffer) → (value : @& Option String) → IO Unit
 
-@[extern "waylean_argument_writer_write_object"]
-opaque ArgumentWriter.writeObject : (writer : @& ArgumentWriter) → (value : @& Option Proxy) → IO Unit
+@[extern "waylean_argument_buffer_write_object"]
+opaque ArgumentBuffer.writeObject : (writer : @& ArgumentBuffer) → (value : @& Option Proxy) → IO Unit
 
-@[extern "waylean_argument_writer_write_new_id"]
-opaque ArgumentWriter.writeNewID : (writer : @& ArgumentWriter) → (value : @& Proxy) → IO Unit
+@[extern "waylean_argument_buffer_write_new_id"]
+opaque ArgumentBuffer.writeNewID : (writer : @& ArgumentBuffer) → (value : @& Proxy) → IO Unit
 
-@[extern "waylean_argument_writer_write_array"]
-opaque ArgumentWriter.writeArray : (writer : @& ArgumentWriter) → (value : @& ByteArray) → IO Unit
+@[extern "waylean_argument_buffer_write_array"]
+opaque ArgumentBuffer.writeArray : (writer : @& ArgumentBuffer) → (value : @& ByteArray) → IO Unit
 
-@[extern "waylean_argument_writer_write_fd"]
-opaque ArgumentWriter.writeFD : (writer : @& ArgumentWriter) → (value : Int32) → IO Unit
+@[extern "waylean_argument_buffer_write_fd"]
+opaque ArgumentBuffer.writeFD : (writer : @& ArgumentBuffer) → (value : Int32) → IO Unit
 
-@[extern "waylean_argument_reader_read_int"]
-opaque ArgumentReader.readInt : (reader : @& ArgumentReader) → IO Int32
+@[extern "waylean_argument_buffer_read_int"]
+opaque ArgumentBuffer.readInt : (reader : @& ArgumentBuffer) → IO Int32
 
-@[extern "waylean_argument_reader_read_uint"]
-opaque ArgumentReader.readUInt : (reader : @& ArgumentReader) → IO Int32
+@[extern "waylean_argument_buffer_read_uint"]
+opaque ArgumentBuffer.readUInt : (reader : @& ArgumentBuffer) → IO Int32
 
-@[extern "waylean_argument_reader_read_fixed"]
-opaque ArgumentReader.readFixed : (reader : @& ArgumentReader) → IO Float
+@[extern "waylean_argument_buffer_read_fixed"]
+opaque ArgumentBuffer.readFixed : (reader : @& ArgumentBuffer) → IO Float
 
-@[extern "waylean_argument_reader_read_string"]
-opaque ArgumentReader.readString : (reader : @& ArgumentReader) → IO (Option String)
+@[extern "waylean_argument_buffer_read_string"]
+opaque ArgumentBuffer.readString : (reader : @& ArgumentBuffer) → IO (Option String)
 
-@[extern "waylean_argument_reader_read_object"]
-opaque ArgumentReader.readObject : (reader : @& ArgumentReader) → IO (Option Proxy)
+@[extern "waylean_argument_buffer_read_object"]
+opaque ArgumentBuffer.readObject : (reader : @& ArgumentBuffer) → IO (Option Proxy)
 
-@[extern "waylean_argument_reader_read_new_id"]
-opaque ArgumentReader.readNewID : (reader : @& ArgumentReader) → IO UInt32
+@[extern "waylean_argument_buffer_read_new_id"]
+opaque ArgumentBuffer.readNewID : (reader : @& ArgumentBuffer) → IO UInt32
 
-@[extern "waylean_argument_reader_read_array"]
-opaque ArgumentReader.readArray : (reader : @& ArgumentReader) → IO ByteArray
+@[extern "waylean_argument_buffer_read_array"]
+opaque ArgumentBuffer.readArray : (reader : @& ArgumentBuffer) → IO ByteArray
 
-@[extern "waylean_argument_reader_read_fd"]
-opaque ArgumentReader.readFD : (reader : @& ArgumentReader) → IO Int32
+@[extern "waylean_argument_buffer_read_fd"]
+opaque ArgumentBuffer.readFD : (reader : @& ArgumentBuffer) → IO Int32
 
 @[extern "waylean_proxy_from_display"]
 opaque Proxy.fromDisplay : (display : Display) → IO Proxy
@@ -137,9 +134,9 @@ opaque Proxy.fromDisplay : (display : Display) → IO Proxy
 opaque Proxy.new : (factory : @& Proxy) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy
 
 @[extern "waylean_proxy_send"]
-opaque Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentWriter : @& ArgumentWriter) → IO Unit
+opaque Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → 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 → ArgumentBuffer → EventLoop M × M) → IO Unit
 
 end Wayland.Native