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/Wayland/Display.lean | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

(limited to 'lib/Wayland/Display.lean')

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
 
-- 
cgit v1.3.1