start implementing wm

5 files changed, 67 insertions, 4 deletions

diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc
index db2983d..940584a 100644
--- a/lib/CWayland/CWayland.cc
+++ b/lib/CWayland/CWayland.cc
@@ -1292,3 +1292,18 @@ lean_obj_res waylean_proxy_get_type(b_lean_obj_arg proxy_obj)
     auto name = wl_proxy_get_interface(proxy)->name;
     return lean_io_result_mk_ok(lean_mk_string(name));
 }
+
+// Proxy.isEqual : (x y : @& Proxy) → Bool
+lean_obj_res waylean_proxy_is_equal(b_lean_obj_arg x, b_lean_obj_arg y)
+{
+    auto x_proxy = static_cast<wl_proxy*>(lean_get_external_data(x));
+    auto y_proxy = static_cast<wl_proxy*>(lean_get_external_data(y));
+    return lean_box(x_proxy == y_proxy ? 1 : 0);
+}
+
+// Proxy.hash : (x : @& Proxy) → UInt64
+lean_obj_res waylean_proxy_hash(b_lean_obj_arg x)
+{
+    auto proxy = static_cast<wl_proxy*>(lean_get_external_data(x));
+    return lean_box_uint64(wl_proxy_get_id(proxy));
+}
\ No newline at end of file
diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h
index 1eeb98f..e4a6897 100644
--- a/lib/CWayland/CWayland.h
+++ b/lib/CWayland/CWayland.h
@@ -83,6 +83,9 @@ lean_obj_res waylean_proxy_listen          (b_lean_obj_arg proxy,
                                             lean_obj_arg   handler);
 lean_obj_res waylean_proxy_keep            (b_lean_obj_arg proxy);
 lean_obj_res waylean_proxy_get_type        (b_lean_obj_arg proxy);
+lean_obj_res waylean_proxy_is_equal        (b_lean_obj_arg x,
+                                            b_lean_obj_arg y);
+lean_obj_res waylean_proxy_hash            (b_lean_obj_arg x);
 
 #ifdef __cplusplus
 }
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 704d7d4..3cfa679 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -416,6 +416,18 @@ def DisplayM.getDisplay' : DisplayM σ (Object "wl_display") := do
 
 variable {ι ι' : InterfaceName}
 
+instance : BEq (Object ι) where
+  beq x y := x.proxy.isEqual y.proxy
+
+instance : Hashable (Object ι) where
+  hash x := x.proxy.hash
+
+instance : BEq AnyObject where
+  beq x y := x.proxy.isEqual y.proxy
+
+instance : Hashable AnyObject where
+  hash x := x.proxy.hash
+
 private def marshalArguments (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : IO (Native.ArgumentBuffer × OpCode) := do
   let argBuffer ← Native.ArgumentBuffer.new
   let opcode : Except String OpCode ← ArgumentBufferM.run (ExceptT.run marshaller) argBuffer
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index b4e9e95..601c709 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -142,4 +142,10 @@ opaque Proxy.keep : (proxy : @& Proxy) → IO Unit
 @[extern "waylean_proxy_get_type"]
 opaque Proxy.getType : (proxy : @& Proxy) → IO String
 
+@[extern "waylean_proxy_is_equal"]
+opaque Proxy.isEqual : (x y : @& Proxy) → Bool
+
+@[extern "waylean_proxy_hash"]
+opaque Proxy.hash : (x : @& Proxy) → UInt64
+
 end Wayland.Native
diff --git a/src/Waylean.lean b/src/Waylean.lean
index 47f9db9..8402351 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -1,23 +1,50 @@
 import Wayland
 import Waylean.Registry
+import Std.Data.HashMap
 
 open Wayland Protocols Waylean
 
+structure Output where
+  removed : Bool
+
 structure State where
   registry : Registry.State := .new
+  outputs : Std.HashMap RiverOutputV1 Output := { }
+
+structure Context where
+  wm : RiverWindowManagerV1
+  xkbBindings : RiverXkbBindingsV1
+
+abbrev WindowManagerM (σ : Type) := ReaderT Context (DisplayM σ)
 
 def zoomRegistry {α : Type} : DisplayM Registry.State α → DisplayM State α :=
   DisplayM.zoom (mk_lens registry)
 
+def handle (ctx : Context) : RiverWindowManagerV1.Event → DisplayM State Unit
+  | .unavailable => do
+      DisplayM.liftIO <| IO.println "Another window manager is already running"
+      DisplayM.requestQuit
+  | .finished => do
+      DisplayM.requestQuit
+  | .manageStart => do
+      let (removedOutputs, aliveOutputs) := (← get).outputs.partition (Function.const _ Output.removed)
+      pure ()
+  | .renderStart => pure ()
+  | .sessionLocked => pure ()
+  | .sessionUnlocked => pure ()
+  | .window win => pure ()
+  | .output out => pure ()
+  | .seat seat => pure ()
+
 def launch : DisplayM State Unit := do
   _ ← DisplayM.registerSignal .SIGINT do
-    DisplayM.liftIO (IO.println "Received SIGINT")
+    DisplayM.liftIO <| IO.println "Received SIGINT"
     DisplayM.requestQuit
-
   zoomRegistry Registry.init
   DisplayM.sync do
-    let shm : WlShm ← zoomRegistry Registry.bindSingleton
-    shm.release
+    let wm : RiverWindowManagerV1 ← zoomRegistry Registry.bindSingleton
+    let xkbBindings : RiverXkbBindingsV1 ← zoomRegistry Registry.bindSingleton
+    wm.listen (handle { wm, xkbBindings })
 
 def main : IO Unit :=
   DisplayM.run launch { }