From 350d3ca21e6a2d215016c84afa07ccb75abd8a6e Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Fri, 5 Jun 2026 17:04:51 +0200
Subject: wip tinyrwm in lean

---
 lib/CWayland/CWayland.cc                           | 14 ++------
 lib/CWayland/CWayland.h                            |  4 +--
 lib/Wayland/Display.lean                           | 23 +++++++------
 lib/Wayland/Native.lean                            |  7 ++--
 .../Protocols/RiverLibinputConfigV1/Header.lean    | 28 ++++++++--------
 .../Protocols/RiverWindowManagementV1/Header.lean  | 32 +++++++++---------
 lib/Wayland/Protocols/Wayland/Header.lean          | 38 +++++++++++-----------
 7 files changed, 68 insertions(+), 78 deletions(-)

(limited to 'lib')

diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc
index f3c966c..08df50b 100644
--- a/lib/CWayland/CWayland.cc
+++ b/lib/CWayland/CWayland.cc
@@ -1299,17 +1299,9 @@ lean_obj_res waylean_proxy_get_type(b_lean_obj_arg proxy_obj)
     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)
+// Proxy.getID : (x : @& Proxy) → IO UInt64
+lean_obj_res waylean_proxy_get_id(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));
+    return lean_io_result_mk_ok(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 e4a6897..ff71348 100644
--- a/lib/CWayland/CWayland.h
+++ b/lib/CWayland/CWayland.h
@@ -83,9 +83,7 @@ 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);
+lean_obj_res waylean_proxy_get_id          (b_lean_obj_arg x);
 
 #ifdef __cplusplus
 }
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 3cfa679..d82a951 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -34,12 +34,14 @@ def Fd : Type := Int32
 /-- Handle to a client object, possibly dead. -/
 structure Object (ι : InterfaceName) : Type where
   private proxy : Native.Proxy
+  private id : UInt64
   deriving Nonempty
 
 /-- Opaque handle to an object whose type is not statically known. -/
 structure AnyObject : Type where
   private proxy : Native.Proxy
   private type : String
+  private id : UInt64
   deriving Nonempty
 
 /-- Monad in which arguments can be marshalled one after another. -/
@@ -278,11 +280,12 @@ private instance : ArgumentDemarshaller (ExceptT String ArgumentBufferM) where
   demarshalString := do (← read).readString
   demarshalObject := do
     let proxy ← (← read).readObject
-    return proxy.map Object.mk
+    proxy.mapM fun proxy ↦ do
+      return ⟨proxy, ← proxy.getID⟩
   demarshalAnyObject := do
     let proxy ← (← read).readObject
     proxy.mapM fun proxy ↦ do
-      return ⟨proxy, ← proxy.getType⟩
+      return ⟨proxy, ← proxy.getType, ← proxy.getID⟩
   demarshalArray := do (← read).readArray
   demarshalFd := do (← read).readFd
 
@@ -412,21 +415,21 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter
 
 def DisplayM.getDisplay' : DisplayM σ (Object "wl_display") := do
   let proxy ← Native.Proxy.fromDisplay (← read).disp
-  return ⟨proxy⟩
+  return ⟨proxy, ← proxy.getID⟩
 
 variable {ι ι' : InterfaceName}
 
 instance : BEq (Object ι) where
-  beq x y := x.proxy.isEqual y.proxy
+  beq x y := x.id == y.id
 
 instance : Hashable (Object ι) where
-  hash x := x.proxy.hash
+  hash x := x.id
 
 instance : BEq AnyObject where
-  beq x y := x.proxy.isEqual y.proxy
+  beq x y := x.id == y.id
 
 instance : Hashable AnyObject where
-  hash x := x.proxy.hash
+  hash x := x.id
 
 private def marshalArguments (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : IO (Native.ArgumentBuffer × OpCode) := do
   let argBuffer ← Native.ArgumentBuffer.new
@@ -445,7 +448,7 @@ def Object.sendConstructor [iface : ResolvedInterface ι'] (obj : Object ι) (ma
   let typeMap := (← read).typeMap
   let (argBuffer, opcode) ← marshalArguments marshaller
   let proxy ← obj.proxy.sendConstructor opcode argBuffer typeMap ι'
-  return ⟨proxy⟩
+  return ⟨proxy, ← proxy.getID⟩
 
 /-- Listen for events from the server for an object. -/
 def Object.listen [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := do
@@ -462,11 +465,11 @@ def Object.keep (obj : Object ι) : DisplayM σ Unit :=
 
 /-- Erase the type information from an object. -/
 def Object.toAny (obj : Object ι) : AnyObject :=
-  ⟨obj.proxy, ι⟩
+  ⟨obj.proxy, ι, obj.id⟩
 
 /-- Try to cast a type-erased object into a typed object. -/
 def AnyObject.cast (obj : AnyObject) : Option (Object ι) :=
-  if obj.type == ι then .some ⟨obj.proxy⟩ else .none
+  if obj.type == ι then .some ⟨obj.proxy, obj.id⟩ else .none
 
 end Proxies
 
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index 601c709..72b0cf2 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -142,10 +142,7 @@ 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
+@[extern "waylean_proxy_get_id"]
+opaque Proxy.getID : (x : @& Proxy) → IO UInt64
 
 end Wayland.Native
diff --git a/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean b/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean
index 3f62b69..48f22dc 100644
--- a/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean
+++ b/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean
@@ -20,9 +20,9 @@ inductive RiverLibinputDeviceV1.Error where
   | invalidArg
 
 structure RiverLibinputDeviceV1.SendEventsModes where
-  enabled : Bool
-  disabled : Bool
-  disabledOnExternalMouse : Bool
+  enabled : Bool := false
+  disabled : Bool := false
+  disabledOnExternalMouse : Bool := false
 
 inductive RiverLibinputDeviceV1.TapState where
   | disabled
@@ -53,10 +53,10 @@ inductive RiverLibinputDeviceV1.AccelProfile where
   | custom
 
 structure RiverLibinputDeviceV1.AccelProfiles where
-  none : Bool
-  flat : Bool
-  adaptive : Bool
-  custom : Bool
+  none : Bool := false
+  flat : Bool := false
+  adaptive : Bool := false
+  custom : Bool := false
 
 inductive RiverLibinputDeviceV1.NaturalScrollState where
   | disabled
@@ -72,9 +72,9 @@ inductive RiverLibinputDeviceV1.ClickMethod where
   | clickfinger
 
 structure RiverLibinputDeviceV1.ClickMethods where
-  none : Bool
-  buttonAreas : Bool
-  clickfinger : Bool
+  none : Bool := false
+  buttonAreas : Bool := false
+  clickfinger : Bool := false
 
 inductive RiverLibinputDeviceV1.ClickfingerButtonMap where
   | lrm
@@ -91,10 +91,10 @@ inductive RiverLibinputDeviceV1.ScrollMethod where
   | onButtonDown
 
 structure RiverLibinputDeviceV1.ScrollMethods where
-  noScroll : Bool
-  twoFinger : Bool
-  edge : Bool
-  onButtonDown : Bool
+  noScroll : Bool := false
+  twoFinger : Bool := false
+  edge : Bool := false
+  onButtonDown : Bool := false
 
 inductive RiverLibinputDeviceV1.ScrollButtonLockState where
   | disabled
diff --git a/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean b/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean
index 4acaf02..4da96e7 100644
--- a/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean
+++ b/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean
@@ -38,17 +38,17 @@ inductive RiverWindowV1.DecorationHint where
   | noPreference
 
 structure RiverWindowV1.Edges where
-  none : Bool
-  top : Bool
-  bottom : Bool
-  left : Bool
-  right : Bool
+  none : Bool := false
+  top : Bool := false
+  bottom : Bool := false
+  left : Bool := false
+  right : Bool := false
 
 structure RiverWindowV1.Capabilities where
-  windowMenu : Bool
-  maximize : Bool
-  fullscreen : Bool
-  minimize : Bool
+  windowMenu : Bool := false
+  maximize : Bool := false
+  fullscreen : Bool := false
+  minimize : Bool := false
 
 inductive RiverDecorationV1.Error where
   | noCommit
@@ -65,13 +65,13 @@ inductive RiverOutputV1.PresentationMode where
   | async
 
 structure RiverSeatV1.Modifiers where
-  none : Bool
-  shift : Bool
-  ctrl : Bool
-  mod1 : Bool
-  mod3 : Bool
-  mod4 : Bool
-  mod5 : Bool
+  none : Bool := false
+  shift : Bool := false
+  ctrl : Bool := false
+  mod1 : Bool := false
+  mod3 : Bool := false
+  mod4 : Bool := false
+  mod5 : Bool := false
 
 namespace RiverWindowManagerV1.Error
 
diff --git a/lib/Wayland/Protocols/Wayland/Header.lean b/lib/Wayland/Protocols/Wayland/Header.lean
index a12c0bf..3d7346d 100644
--- a/lib/Wayland/Protocols/Wayland/Header.lean
+++ b/lib/Wayland/Protocols/Wayland/Header.lean
@@ -201,27 +201,27 @@ inductive WlDataDevice.Error where
   | usedSource
 
 structure WlDataDeviceManager.DndAction where
-  none : Bool
-  copy : Bool
-  move : Bool
-  ask : Bool
+  none : Bool := false
+  copy : Bool := false
+  move : Bool := false
+  ask : Bool := false
 
 inductive WlShell.Error where
   | role
 
 structure WlShellSurface.Resize where
-  none : Bool
-  top : Bool
-  bottom : Bool
-  left : Bool
-  topLeft : Bool
-  bottomLeft : Bool
-  right : Bool
-  topRight : Bool
-  bottomRight : Bool
+  none : Bool := false
+  top : Bool := false
+  bottom : Bool := false
+  left : Bool := false
+  topLeft : Bool := false
+  bottomLeft : Bool := false
+  right : Bool := false
+  topRight : Bool := false
+  bottomRight : Bool := false
 
 structure WlShellSurface.Transient where
-  inactive : Bool
+  inactive : Bool := false
 
 inductive WlShellSurface.FullscreenMethod where
   | default
@@ -237,9 +237,9 @@ inductive WlSurface.Error where
   | defunctRoleObject
 
 structure WlSeat.Capability where
-  pointer : Bool
-  keyboard : Bool
-  touch : Bool
+  pointer : Bool := false
+  keyboard : Bool := false
+  touch : Bool := false
 
 inductive WlSeat.Error where
   | missingCapability
@@ -293,8 +293,8 @@ inductive WlOutput.Transform where
   | flipped270
 
 structure WlOutput.Mode where
-  current : Bool
-  preferred : Bool
+  current : Bool := false
+  preferred : Bool := false
 
 inductive WlSubcompositor.Error where
   | badSurface
-- 
cgit v1.3.1