4 files changed, 59 insertions, 16 deletions
diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc
index 8fae40c..ecb87fc 100644
--- a/lib/CWayland/CWayland.cc
+++ b/lib/CWayland/CWayland.cc
@@ -122,6 +122,23 @@ namespace
     }
 }
 
+// -- Constants
+
+uint32_t waylean_SIGINT(void)
+{
+    return SIGINT;
+}
+
+uint32_t waylean_SIGUSR1(void)
+{
+    return SIGUSR1;
+}
+
+uint32_t waylean_SIGUSR2(void)
+{
+    return SIGUSR2;
+}
+
 // -- Display
     
 namespace
diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h
index 52106f2..75d2e0d 100644
--- a/lib/CWayland/CWayland.h
+++ b/lib/CWayland/CWayland.h
@@ -7,12 +7,18 @@ extern "C"
 {
 #endif
 
-// Display
+// -- Constants
+
+uint32_t waylean_SIGINT(void);
+uint32_t waylean_SIGUSR1(void);
+uint32_t waylean_SIGUSR2(void);
+
+// -- Display
 
 lean_obj_res waylean_display_new      (b_lean_obj_arg name);
 lean_obj_res waylean_display_roundtrip(b_lean_obj_arg display);
 
-// Event Loop
+// -- Event Loop
 
 lean_obj_res waylean_event_loop_new        (void);
 lean_obj_res waylean_event_loop_add_display(b_lean_obj_arg event_loop,
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index d2c3e33..95d1739 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -1,3 +1,18 @@
+namespace Wayland.Native
+
+@[extern "waylean_SIGINT"]
+private opaque _SIGINT (u : Unit) : UInt32
+
+@[extern "waylean_SIGUSR1"]
+private opaque _SIGUSR1 (u : Unit) : UInt32
+
+@[extern "waylean_SIGUSR2"]
+private opaque _SIGUSR2 (u : Unit) : UInt32
+
+def SIGINT: UInt32 := _SIGINT ()
+def SIGUSR1: UInt32 := _SIGUSR1 ()
+def SIGUSR2: UInt32 := _SIGUSR2 ()
+
 private opaque DisplayP : NonemptyType
 def Display : Type := DisplayP.type
 instance : Nonempty Display := DisplayP.property
@@ -8,31 +23,35 @@ opaque Display.new : (name : @& Option String) → IO Display
 @[extern "waylean_display_roundtrip"]
 opaque Display.roundtrip : (display : @& Display) → IO Unit
 
-private opaque EventLoopP : NonemptyType
-def EventLoop : Type := EventLoopP.type
-instance : Nonempty EventLoop := EventLoopP.property
+variable {M : Type}
+
+private opaque EventLoopP (M : Type) : NonemptyType
+def EventLoop (M : Type) : Type := (EventLoopP M).type
+instance : Nonempty (EventLoop M) := (EventLoopP M).property
 
 private opaque EventSourceP : NonemptyType
 def EventSource : Type := EventSourceP.type
 instance : Nonempty EventSource := EventSourceP.property
 
 @[extern "waylean_event_loop_new"]
-opaque EventLoop.new : IO EventLoop
+opaque EventLoop.new : IO (EventLoop M)
 
 @[extern "waylean_event_loop_add_display"]
-opaque EventLoop.addDisplay : (eventLoop : @& EventLoop) → (display : @& Display) → IO EventSource
+opaque EventLoop.addDisplay : (eventLoop : @& (EventLoop M)) → (display : @& Display) → IO EventSource
 
 @[extern "waylean_event_loop_add_timer"]
-opaque EventLoop.addTimer : (eventLoop : @& EventLoop) → (delayMs : UInt32) → (msg : @& IO Unit) → IO EventSource
+opaque EventLoop.addTimer : (eventLoop : @& (EventLoop M)) → (delayMs : UInt32) → (msg : @& M) → IO EventSource
 
 @[extern "waylean_event_loop_add_signal"]
-opaque EventLoop.addSignal : (eventLoop : @& EventLoop) → (signum : UInt32) → (msg : @& IO Unit) → IO EventSource
+opaque EventLoop.addSignal : (eventLoop : @& (EventLoop M)) → (signum : UInt32) → (msg : @& M) → IO EventSource
 
 @[extern "waylean_event_loop_remove"]
-opaque EventLoop.remove : (eventLoop : @& EventLoop) → (source : @& EventSource) → IO Unit
+opaque EventLoop.remove : (eventLoop : @& (EventLoop M)) → (source : @& EventSource) → IO Unit
 
 @[extern "waylean_event_loop_quit"]
-opaque EventLoop.quit : (eventLoop : @& EventLoop) → IO Unit
+opaque EventLoop.quit : (eventLoop : @& (EventLoop M)) → IO Unit
 
 @[extern "waylean_event_loop_poll"]
-opaque EventLoop.poll : (eventLoop : @& EventLoop) → IO (Option (IO Unit))
+opaque EventLoop.poll : (eventLoop : @& (EventLoop M)) → IO (Option M)
+
+end Wayland.Native
diff --git a/src/Waylean.lean b/src/Waylean.lean
index 28c5f58..a13b867 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -1,15 +1,16 @@
 import Wayland
+open Wayland.Native
 
-partial def mainLoop (loop : EventLoop) : IO Unit := do
+partial def mainLoop (loop : EventLoop (IO Unit)) : IO Unit := do
   match (← loop.poll) with
   | .none => return
   | .some msg => msg; mainLoop loop
 
 partial def main : IO Unit := do
-  let disp ← Display.new .none
-  let loop ← EventLoop.new
+  let disp : Display ← Display.new .none
+  let loop : EventLoop (IO Unit) ← EventLoop.new
   _ ← loop.addDisplay disp
-  _ ← loop.addSignal 2 (do
+  _ ← loop.addSignal SIGINT (do
     IO.println "Received SIGINT"
     loop.quit)
   let rec setUpTimer := loop.addTimer 500 (do