type map implementation

1 files changed, 23 insertions, 0 deletions

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