diff options
Diffstat (limited to 'lib/Wayland/Native.lean')
| -rw-r--r-- | lib/Wayland/Native.lean | 23 |
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 |